Tauto Book：解説とリファレンス
値と関数から所有権・代数的効果・依存型・定理証明へ進む24章と、学習ガイド・仕様索引・検証の手引き。順に学ぶときにも、規則を調べるときにも使える本です。
- この本の使い方と学習の道筋
- Tauto という言語
- 最初のプログラム
- 値・変数・基本型
- 関数と制御フロー
- 構造体・列挙型・パターンマッチ
- リスト・ジェネリクス・型クラス
- 所有権の四つの種
- 借用と参照
- 代数的効果とは何か
- 継続の回数と所有権
- 実行の上限を設定する
- プロジェクト・テスト・ツール
- 証明の第一歩
- 等式を証明する
- 帰納法と再帰
- タクティクと証明のステップ
- 依存型と型の宇宙
- 数学の証明を書く
- 実例：ソートの正しさ
- 実例：状態遷移と不変条件
- 実例：型付きミニ言語を作る
- 何が保証され、何が保証されないか
- これから何を作るか
- 付録A 構文早見表
- 付録B 演習のヒントと解答
- 付録C 用語集と学習チェックリスト
- 付録D 意味論・仕様索引
- 付録E 実行・検証の手引き