Leanで正規表現エンジンをつくる。そして正しさを証明する
定理証明支援系として: 数学の 定理 やプログラムの 性質 、それらの証明を記述する言語 https://gyazo.com/ebd3b09772c6c8d69e7c77b59f95d816
Lean 上で実装が正しいことを検証
実装が正しい？
マッチの仕様を厳密に定義し、それを合致することを示す
Lean の最適化
2 つの実行モデル
参照カウンタを見るとデータ構造の更新を 破壊的変更 に最適化できる パズル的な面白さ
深い理解が得られる
これが一番重要
証明を書くにはなぜ定理が成立するかを理解しなければならない
書いたプログラムがなぜ正しく動くのかを深く理解する必要がある
プログラムはなぜ正しく動くのか？ = 良い 不変条件 が成立しているから 不変条件 = プログラムの各ステップの前後で常に成立している性質
性質はどう見つけるか？
1. 不変条件を見つける
2. 各処理が見つけた不変条件を保存することを示す
3. 見つけた不変条件が所望の性質を導くことを示す
どう不変条件を見つけるか？: 具体例や欲しい性質から逆算する