これから何を作るか
学んだ道具を、一つの小さな検証済みプログラムにまとめます。
21.1 おすすめの学習プロジェクト
最初から大きな定理を証明する必要はありません。入力が少なく、状態と遷移がはっきりしたものから始めると、プログラムの意味と定理の関係がつかみやすくなります。
| 題材 | 最初の実装 | 次に書く定理 |
|---|---|---|
| カウンター | Nat の増減 | 0 より小さくならない |
| フラグ管理 | open / closed の切り替え | closed では減算しない |
| リスト反転 | 再帰的な reverse | 二回反転すると元に戻る |
| 最大値 | 比較による選択 | どちらの入力以上でもある |
| ソート | insert と sort | 整列と要素の保存 |
21.2 問題を小さく分ける
開発は、次の順に進めると効率的です。
- 仕様：何が成り立てば成功か、日本語で明確にする。
- 型とデータ：状態や入力の取り得る形を、
enum・structで表す。 - 純粋な処理：できるだけ副作用を分離して、
fnを書く。 - 簡単な例：
runとtestで、意図した動作を確認する。 - 命題：
theoremとEqなどで、不変条件を宣言する。 - 証明：構成子での
match・補題・等式の書き換えを使う。 - 境界：外部の操作や、実行環境に依存する部分を書き出す。
21.3 次の段階へ
リポジトリの examples/ には、この本で触れた題材の、もっと大きな例があります。
sort/：任意のOrdな型に使える挿入ソートと、その証明。bst/：二分探索木（集合）と、その証明。compiler/：算術式をスタックマシンに変換する処理と、その正しさの証明。effect-proofs/：代数的効果のハンドラが、証明済みの遷移を呼ぶ例。certified-state/：証明した状態遷移と、実行側を結ぶ例。
自然数の演算が分かったら、Prop・inductive・Type の関係を深めてみてください。効果の表現力に興味があるなら、resume ω が状態や所有権に与える影響を調べるのが良い練習になります。
最後に一つ。定理の名前を大きくするより、前提と結論を、正確に小さく書くことを重視してください。それが、Tauto らしい「読めて、機械的に確かめられるソフトウェア」につながります。