信頼

Lean が提供する価値の大部分は、プログラムの正しさに関する証明を含む数学的証明を構築する能力です。これに対するユーザの一般的な疑念は、Lean を信頼するには、具体的に何をどの程度信頼すればよいのかということです。

この質問に対する回答は2つの部分からなります：すなわち、Lean における証明を信頼するためにユーザがまず信頼すべきものは何かということ、そして Lean プログラムをコンパイルして得られる実行可能プログラムを信頼するためにユーザが信頼すべきものは何かということです。

この違いは具体的には、証明（プログラムに関する文を含む）とコンパイルされていないプログラムが Lean のカーネル言語で直接表現でき、カーネルの実装によってチェックされるというものです。これらは実行ファイルにコンパイルする必要はなく、そのため、この信頼はこれらをチェックするカーネルの実装に限定され、Lean のコンパイラは信頼できるコードベースの一部にはなりません。

コンパイルされた Lean プログラムの正しさを信頼するには、Lean のコンパイラを信頼する必要がありますが、コンパイラはカーネルとは別物であり、Lean のコアロジックの一部ではありません。ここで Lean の 文とプログラム を信頼することと、Lean のコンパイラが生成したプログラム を信頼することは区別されます。Lean のプログラムに関する文は証明であり、カーネルだけを信頼すればよいカテゴリに入ります。プログラムに関する証明が コンパイルされたプログラムの動作にまで及ぶこと を信頼することで、コンパイラは信頼されるコードベースに入ります。

注意：タクティクや他のメタプログラムは、たとえコンパイルされたタクティクであっても信頼される必要は 全くありません；これらは他で使用されるカーネルの項を生成するために使用される信頼されていないコードです。ある命題 P は信頼されたコードベースをカーネルを超えて拡張することなく、任意に複雑なコンパイル済みのメタプログラムを使って証明することができます。なぜならこのメタプログラムは Lean のカーネル言語で表現された証明を生成する必要があるからです。

  • これらの文は エクスポートされた 証明に対して有効です。より くどい 警戒心の強い読者を満足させるために、これは例えば、エクスポータと検証器を実行するために使用されるコンピュータの OS・ハードウェアなどに対するある程度の信頼を必然的に伴います。
  • エクスポートされていない証明については、ユーザはさらにカーネル外の Lean の要素（エラボレータ、パーサなど）を信頼することになります。

より詳細なリスト

Lean 4 に関連する信頼について、Mario Carneiro による Lean の Zulip への投稿からより詳細に説明しましょう。

一般的に：

  1. Lean のロジックが健全であること（原著者注：これには Nat や String のようなカーネルの拡張も含まれる）を信頼する。

  2. プログラムの正しさを証明しなかった場合、エラボレータがあなたの入力から期待するプログラムを示す Lean の式に変換したことを信頼する。

  3. プログラムが正しいことを証明したのであれば、そのプログラムに関する証明がチェックされていることを信頼する（これを排除するために外部のチェッカを使う）。

  4. これらすべてを動かしているハードウェア・ファームウェア・OS ソフトウェアが壊れたり、嘘をついたりしていないことを信頼する。

  5. （プログラムを実行する時）ハードウェア・ファームウェア・OS ソフトウェアが仕様通りに忠実にプログラムを実行し、デバッガやハードディスク上の磁石や宇宙線がプログラムの出力を乱すことがないことを信頼する。

複雑な実行ファイルについて：

  1. コンパイラのオーバーライド（extern・implemented_by）がLean のロジックに違反しないことを信頼する（すなわち、モデルが実装と一致する）。

  2. Lean のコンパイラ（Lean コードを C に変換）がプログラムの意味を維持することを信頼する。

  3. C プログラムを同じ意味を持つ実行ファイルに変換する clang・LLVM を信頼する。

前半のポイントは証明とコンパイルされた実行ファイルの両方に適用され、後半のポイントは特にコンパイルされた実行ファイルに適用されます。

外部チェッカへの信頼

  1. Lean のロジックが健全であることをとにかく信頼する。
  1. 外部チェッカの開発者が適切にプログラムを実装していることを信頼する。
  1. 実装言語のコンパイラやインタプリタを信頼する。複数の外部チェッカを実行する場合、それらをベン図の円のように考えることができます；円が交差する部分に健全性の問題がないことを信頼します。
  1. Nat と String のカーネル拡張について、おそらく実装言語の bignum ライブラリと UTF-8 文字列型を信頼する。

外部チェッカを使用する利点は以下の通りです：

  • ユーザは Lean のエコシステムから切り離され、Lean のコードベースのどの部分にも依存しないものを使って結果をチェックすることができます。
  • 外部チェッカは成熟したコンパイラやインタプリタを利用するように書くことができます。
  • カーネル拡張に対しては、ユーザは複数の bignum・string 実装の結果をクロスチェックできます。
  • エクスポート機能を使うことは、Lean のカーネル外の部分を信頼することから抜け出す唯一の方法です。したがって、エクスポートされたファイルが lean4lean のようなものによってチェックされたとしてもこれを行うことには利点があります。それゆえ Lean のメタプログラミング機能の誤用による影響を心配するユーザはエクスポート機能を使うことが推奨されます。