Himmel さんのスライド

[Seasawher]

https://github.com/TwoFX/berlin2026

[Seasawher]

https://github.com/TwoFX/berlin2026/blob/master/Bobkonf/Slides.lean

このスライドの主張を要約して

一言でいうと

このスライドの中心的な主張は、

Leanでは、証明はプログラムの正しさを後から確認するだけでなく、実際にコンパイルされるコードを安全かつ高速にするための情報として利用できる

というものです。

証明によって「この分岐は絶対に起きない」「この配列アクセスは必ず範囲内」「このバイト列は必ず正しいUTF-8」と保証できれば、実行時チェックや失敗処理をコンパイラが除去できます。

1. Leanには「プログラム」と「証明」の明確なフェーズ分離がない

スライドでは、プログラム検証の方法をおおむね次の三つに分類しています。

1. RustやCなどで書き、Lean・Isabelle・SMT向けの検証条件を生成する
2. DafnyやRocqなどで書き、通常の言語へコード抽出する
3. Idris 2やLean 4のような、検証機能を持ったプログラミング言語で直接書く

Leanの特徴は三番目であり、実行用コードと証明を同じ言語・同じプログラムの中に置けることです。スライドはこれを「コードと証明の間に phase separation がない」と表現しています。

2. 証明をプログラムの中に埋め込める

例えば配列アクセスには、概念的に三種類があります。

• 証明を要求し、実行時チェックを行わない安全なアクセス
• 実行時チェックを行い、Optionを返すアクセス
• 実行時チェックを行い、範囲外ならpanicするアクセス

範囲内であることをLeanに証明させれば、利用者は安全なアクセスを使いながら、実行時チェックのコストを避けられます。自動証明が十分強ければ、証明を毎回手作業で書く必要もありません。

ここで重要なのは、証明が実行時にも持ち回られるわけではないことです。配列アクセスは最終的にはC++ランタイムの高速な関数を呼びますが、その前にLeanの型検査器が安全性を保証します。実行時には型や証明は消去されています。

つまり、

検査はコンパイル時に行い、実行時にはunsafe相当の高速な処理を安全に呼ぶ

という構造です。

3. 「起こり得ない分岐」を証明によって削除できる

通常のプログラムでは、論理的には起こり得ない分岐にも、panicなどの処理を書かなければならない場合があります。

Leanでは、矛盾した仮定からFalseの証明を作り、空の型でパターンマッチすることで、その分岐が不可能であることを明示できます。空の型には値が存在しないため、分岐の実装も存在しません。

さらに、引数の型や前提条件から不可能性が明らかな場合、Leanが自動的に不可能なケースを処理し、コンパイラがその分岐自体を消去できます。

Rustのunreachable_uncheckedに似ていますが、Rustでは安全性の根拠がコメントとプログラマの責任に置かれます。Leanでは、その前提を関数の型に書き、機械的に検査できます。

4. 実例1：平衡二分探索木

Lean標準ライブラリのweight-balanced treeでは、木を回転して再平衡化する際に、非常に複雑なパターンマッチが発生します。

平衡性の証明がなければ、「本来は起きないはずの木の形」に対しても実行時チェックやpanicを残す必要があります。

平衡性と再平衡化関数の事前条件を証明として渡すと、不可能なケースをFalse.elimで処理でき、コンパイラがその分岐を除去できます。スライドによれば、この変更によって実行速度が測定可能な範囲で約3%改善しました。

ここでは証明が単なる安全性保証ではなく、最適化を正当化する証明書として機能しています。

5. 実例2：UTF-8文字列

Leanの文字列は、単なるバイト列ではなく、概念的には次の組です。

• UTF-8で符号化されたバイト列
• そのバイト列が正しいUTF-8であるという証明

したがって、すべてのStringは構築された時点でUTF-8妥当性を持っています。文字列連結などの操作は、データとともにその不変条件の証明も伝播させます。

有効な文字位置であることまで型と証明で分かっていれば、文字のデコードが成功することも静的に証明できます。そのため、実行時にOptionを返したり、エラー分岐を設けたりせず、高速なデコード関数を直接呼べます。スライドでは識別子補完などで実用上認識できる性能差があると述べています。

ただし、これを実現するには、ビットベクトル、UTF-8のバイト単位の仕様、合成可能な補題、ライブラリ操作との接続など、相当量の理論整備が必要です。

6. 単純な「検証条件生成」より理論構築を重視している

発表者は、平衡木と文字列では証明のスタイルが異なると整理しています。

• 平衡木：抽象化を外し、simp・omega・場合分けなどでSMT的に解く
• UTF-8文字列：再利用可能な理論や補題を体系的に構築する

そして発表者の見解として、単発のverification conditionを解くことより、再利用可能な理論を構築する方が遠くまで進めると述べています。

そのうえで、実用的な証明環境には次の三つが必要だと主張しています。

• 対話的である
• 高度に自動化されている
• 自動化の動作が人間に理解できる

結論

スライド全体の主張を整理すると、次のようになります。

証明付きプログラミングは、「安全性のために実行速度を犠牲にする」方法ではない。
証明によって実行時チェック、不可能な分岐、失敗処理を安全に除去できるため、安全性と性能を同時に得られる。

また、コードと証明を同じ場所で発展させられるLeanの設計には大きな利点がある一方、最後には、

プログラムと証明を混在させる利点を維持しつつ、両者を別々に保守することは可能か

という未解決の設計上の問いを提示しています。

要するにこれは、**「証明はテストや仕様書の強化版ではなく、コンパイラが利用できるゼロコストの実行時情報である」**という発表です。

[Seasawher]

Coq のように証明とコードが分離していると何が困るの？

まず、Coqでも証明とコードは同じ項の中に書けます。問題は主に、実行時コードを得る段階で extraction を挟み、証明世界と実行世界を分離することです。

困るのは、証明ができないことではなく、証明を実装や最適化に細かく反映しにくいことです。

1. 証明を使って安全な低レベル処理を直接選びにくい

たとえば配列アクセスについて、

i < array.length

が証明済みなら、実行時の境界チェックを省略してよいはずです。

Leanでは概念的に、

array[i]'(proof)

と書き、型検査時に証明を確認したうえで、実行時にはuncheckedな配列アクセスを呼べます。証明自体は消去されるので、実行時コストはありません。

一方、CoqからOCamlなどへ抽出する場合、証明は通常消去されますが、抽出後のOCamlコンパイラは、

このアクセスがCoq側で範囲内だと証明されていた

という事情を基本的には知りません。

そのため、抽出後のコードで通常の安全な配列アクセスを使えば境界チェックが残り、uncheckedな処理を使うなら、抽出設定や手書きコードとの接続が必要になります。

つまり、

証明は正しさを保証するが、証明がそのままコード生成上の選択を制御するとは限らない

ということです。

2. 「不可能な分岐」が抽出後に復活しやすい

依存型によって、ある分岐が論理的に不可能だと証明できる場合があります。

Leanではその分岐をFalseから除去でき、コンパイラも実際に分岐そのものを消せます。スライドの平衡木の例では、この仕組みによって本来あり得ないpanic分岐を除去し、約3%の性能改善が得られています。

Coqの抽出では、依存型や証明が消去された後、出力先言語の型だけを見ると、元は不可能だったケースが型の上では再び表現可能になることがあります。

すると抽出器は、場合によっては次のような形を残さざるを得ません。

match x with
| PossibleCase -> ...
| ImpossibleCase -> assert false

Coqでは不可能性が証明されていても、抽出後の言語の型システムだけではそれを表現できないからです。

3. データの不変条件が出力先の型から失われる

スライドのUTF-8文字列では、文字列が概念的に、

structure String where
bytes : ByteArray
validUTF8 : IsValidUTF8 bytes

という、データと不変条件の組になっています。すべての文字列操作が、その証明を次の操作へ伝播させます。

Coqでも同様の構造は書けますが、抽出時にvalidUTF8が証明として消去されれば、抽出後には単なるバイト列になります。

その結果、OCaml側の型だけでは、

このバイト列は必ず正しいUTF-8である

とは分かりません。

したがって、抽出されたコードをOCaml側でさらに加工したり、別の関数と組み合わせたりすると、その不変条件は型によって保護されません。正しさは、あくまで「Coqから生成された部分を規定通り使う」という境界に依存します。

4. コードと証明を一緒にリファクタリングしにくい

Leanでは、実装を変更すると証明義務がその場で発生します。

たとえば、

min left.size right.size

を

max left.size right.size

に変えれば、配列アクセスの安全性がその場で破れ、エディタ上でエラーになります。

コードと証明が同一の型検査・コンパイルパイプラインにあるため、

• 実装を変える
• 証明義務が変わる
• 自動化で直す
• 生成コードも変わる

というサイクルが一体化しています。

抽出型の開発では、

• Coq内部の証明付きプログラム
• 抽出設定
• 抽出されたOCamlコード
• 手書きランタイムやFFI

という複数の層ができます。最適化や実装変更が層をまたぐと、保守対象が増えます。

5. 出力先コンパイラは証明を理解しない

Coq側では、

• この値は0ではない
• このリストは空でない
• この木は平衡している
• このインデックスは範囲内である

と証明できています。

しかし抽出後、OCamlやHaskellのコンパイラに見えるのは、証明が消去された通常のデータだけです。

したがって、出力先コンパイラが同じ事実を独自の解析で再発見できなければ、証明を使った最適化は行えません。

Leanの主張は、

既に人間と証明器が知っている事実を、通常のコンパイラにもう一度推測させる必要はない

というものです。証明をコンパイラの入力として直接利用できます。

ただし、分離には利点もある

分離は単なる欠点ではありません。

Coqの抽出方式には、

• 実行先として成熟したOCamlやHaskellを使える
• 証明用の機構を実行系から切り離せる
• 数学的仕様と実装の境界を明確にできる
• 証明支援系のランタイム設計に拘束されにくい

という利点があります。

したがって対立は、

Coq: 証明されたプログラムを、通常言語へ移す
Lean: 証明とプログラムを、同じコンパイル系の中で共同利用する

という設計上のトレードオフです。

本質

最も大きな違いは次です。

Coq的な抽出では、証明は主に「生成前の正しさの保証」である。
Leanでは、証明を「生成されるコードの形を決める情報」にもできる。

したがって、証明とコードの分離で困るのは、正しさの証明そのものではなく、証明を使って実行時チェックを除去したり、不可能な分岐を消したり、低レベル実装を安全に利用したりする際の距離が遠くなることです。