型・仕様・証明は「禁止と保証」でつながる
要点：理論は“賢くなる話”というより、保守と説明がラクになる話です。
このページは、メルマガ第6通目（型・仕様・証明）を補助する固定ページです。
読み終えるころには、次の1行が自然に出る状態を目指します。
「ここで禁止したい操作は何？ 何を保証したい？」
30秒要約
- 仕様：入力と出力の契約（期待と制約）
- 型：許される操作／許されない操作（禁止と保証）
- 証明：その保証が崩れない根拠（壊れない手順）
違う言葉に見えますが、全部「禁止と保証」を明文化して、雰囲気をチェック可能に寄せる道具です。
まず、三者はこう対応する
仕様（Spec）
- 「何を受け取り、何を返すか」を文章やテストで固定する
- 境界条件・例外・前提（precondition）・結果（postcondition）を明文化する
役割：期待と制約を決める（契約）
型（Type）
- 「それはやっていい／それはやるな」を表現のレベルで制約する
- “正しい形”を値の世界に押し込むことで、ミスの可能性を減らす
役割：禁止と保証を、機械でチェックできる形にする
証明（Proof）
- 「その保証は本当に崩れない」を、手順として示す
- 広義には、厳密な証明だけでなく、テスト・検証・レビュー指針も近縁
役割：保証が崩れない根拠（壊れない手順）を与える
ひとつの主張を、三段階で固める（ミニ例）
雰囲気の主張：
「この関数は、必ず正しい形のデータを返す」
この“雰囲気”は、段階的に固められます。
1) 仕様で固める
- どんな入力を受け付けるか
- どんな出力を返すか
- 例外／エラー条件は何か
ここで初めて「正しい形」が、他人と共有できる言葉になります。
2) 型で固める
- 不正な形のデータを 返せない 形に設計する
- たとえば「nullable を返さない」「状態を型で分ける」「不変条件を表現で守る」
型は“説明”というより、禁止の柵です。
3) 証明（広義）で固める
- 境界ケースでも仕様が崩れないことを確認する
- 反例を潰す（条件追加・前提の明確化）
- 必要なら形式的な証明へ（ただし最初から必須ではない）
ここまで行くと、変更に強い設計になります。
実務での嬉しさは、だいたいこの3つ
- レビューが速くなる：何が保証されているかが明確
- 変更に強くなる：壊れる場所が局所化される（影響範囲が読める）
- 説明が短くなる：例外や但し書きが減る／言葉が揃う
理論の旨味は、知識量ではなく「保守と説明コストの低下」に出ます。
よくある誤解を1つだけ外す
「証明」は“作文”ではない。
証明は、
許された操作（ルール）だけで、ゴールまで到達する手順です。
文章が難しく見えるのは、手順が見えていないから。
手順として見れば、反例→条件追加→更新、という実務の流れに近づきます。
今日の1行（ここだけ持ち帰る）
次に設計で迷ったら、メモにこれだけ書いてください。
「ここで禁止したい操作は何？ 何を保証したい？」
この1行が出ると、型・仕様・証明は“自分ごと”になります。
補助資料（任意）
- 1枚カードPDF：型・仕様・証明「禁止と保証」まとめ
PDFを開く
[[PDF_URL]]例：https://ronkeisha.net/assets/pdf/type-spec-proof-card.pdf
次の一歩
© Ronkeisha / 論計舎