この本の使い方と学習の道筋
Tauto Book は、順に理解を積み上げる解説と、必要な規則に戻るためのリファレンスを分けて使う本です。証明だけを先に覚える必要はありません。まず小さなプログラムを動かし、その振る舞いのうち何を型や命題で表現するかを学びます。
0.1 三つの入口
- 初めて読む：第1章から始めます。以下の到達目標を使い、章末の演習と自分のコードで理解を確認してください。
- 規則を調べる：意味論・仕様索引から、型・所有権・効果・証明の規則と境界を探します。綴りだけを思い出すなら構文早見表を使います。
- 手元のコードが通らない：実行・検証の手引きで、型検査・証明・実行・バックエンドのどこで失敗しているかを切り分けます。
本文は読むための教材です。このページ内でのコード編集、再検査、学習進捗の保存は行いません。Playgroundまたは手元の CLI で試してください。
0.2 順に読むコース
| 範囲 | 前提 | 読後にできること | 自分で確かめること |
|---|---|---|---|
| 1–2章：最初の実行 | プログラミング経験は不要 | ファイルを作り、出力を確認する | 入力や定数を変えると出力がどう変わるか |
| 3–6章：データと関数 | 最初のプログラムを実行できる | 分岐、レコード、列挙、リスト、汎用関数を組み合わせる | 空のデータ、分岐の両側、再帰の終端を扱えるか |
| 7–8章：値の使用規則 | 関数とデータ構造 | 所有権の種類と借用を区別して API を読む | 値の移動と、借用終了後の再使用を説明できるか |
| 9–11章：効果と実行上限 | 借用と所有権 | 効果の要求と処理を分け、継続と予算の制約を読む | 処理しなかった効果と、予算を使い切る経路は何か |
| 12章：プロジェクト | 小さな実行プログラム | ファイルを分け、テストと検査を使い分ける | 表示しただけの出力を、検証したと誤解していないか |
| 13–17章：証明の基礎 | 関数、型、match | 命題を型として読み、等式・帰納法・依存型を使う | 定理の仮定と結論を、自分の言葉で言えるか |
| 18–20章：保証の組み立て | 証明の基礎 | アルゴリズムや状態遷移の性質を述べ、保証の境界を区別する | 証明した関数と、実際に呼ぶ関数は同じか |
| 21章：次のプログラム | 上記の検査と実行の区別 | 小さな実用プログラムの中心と外部境界を設計する | 入出力やバックエンドのどこをテストで補うか |
全章を同じ速さで読む必要はありません。既にプログラミングに慣れているなら1–6章の例を動かしてから、7章の所有権へ進めます。証明から読み始める場合も、5章の match、6章の型パラメータ、12章の検査コマンドを先に確認してください。
0.3 一章を終える手順
- 掲載例のファイル名と
importを保って実行します。同じファイル名の後続ブロックは、前のブロックに続けて読む例があります。 - 入力を一つ変え、結果を予想してから実行します。
- 演習に答え、ヒントと解答と比べます。答えだけでなく、成り立つ理由を説明します。
- 用語集・チェックリストを使って、説明できない言葉を前の章へ戻って調べます。
- 証明の章では、命題を強くしたり仮定を外したりしたとき、本当に検査が通るかを確認します。穴を残した状態を完成扱いしません。
0.4 検査結果の読み方
例に付いた結果は、サイト生成時に特定の CLI で取得した記録です。読者の環境で今実行した結果でも、すべてのバックエンドでの互換性保証でもありません。意図的に失敗する例や、証明穴を残した例には、その状態を表示します。
skipped は証明カーネルの対象外という分類です。「実行プログラムの検査をすべて省略した」とも、「実行まで成功した」とも読み替えないでください。型検査、命題の証明、テスト、実行結果は別々に確認します。
0.5 本の範囲と仕様の確認
この本は説明と参照の入口です。完全な規範仕様や、将来の構文の約束ではありません。新しい設計案は、実装されて検査された構文と区別します。例が通らないときは、CLI のバージョン、ファイル全体、コマンド、診断を記録し、検証の手引きに従って切り分けてください。