TL;DR ── この記事が明らかにすること
想定読者
この記事を読む価値
第１部 ── 形式手法という森の地図
- ４つの系統は、どう違うのか？
- （１つ目）対話的証明支援系
- （２つ目）仕様に基づく自動検証
- （３つ目）静的解析・モデル検査
- （４つ目）ハードウェア検証
第２部 ── 機械で足りる場面と、人が仕様を書くしかない場面
- 分かれ目は「有限か無限か」ではありません
- 本当の分かれ目は、２つの問いにあります
- では、「性質を自分で書き下す必要がある」場面とは、具体的に何か
- この４つに共通する構図
第３部 ── では、日本はどうだったのか
- 理由１ ── 日本が強いのは、性質があらかじめ決まっている領域
- 理由２ ── 基盤層を作る産業構造が、欧米とは異なっていた
- ただし ── 日本にも、基盤にあたる技術はあります
- まとめると
そして ── これが本記事の後半の主題ですが ── AI の出力を検証するという領域は、まさに「どんな入力が来るか分からない」新しい基盤層です。そこでは、まだどの国も先行を確定させていません。
第４部 ── これらの言語は、マイナーなのか
- 数学研究の最前線
- 産業の基盤層
- 実務で使われている業界
第５部 ── キャリアにつながるのか
- Python の型ヒントから、証明支援系へ
- 伸び筋は、３つの方向にあります
- 「LLM が賢いなら、機械が全部やればいいのでは？」
- では、仕様そのものも AI に書かせればよいのでは？
  - まず、退けておくべき答え ── 「AI は嘘をつくから」
  - 本当の理由 ── 「仕様が正しいか」は、形式的な問いではないから
具体的に、何が起きるのか ── ３つの失敗の形
人間が引き受けるべき役割とは？
- Physical AI と AI エージェント ── 伸びるのは、どちらの手法か
- 知覚と制御の層 ── ここは、機械が自動で調べる手法の領域
- 方針と規則の層 ── ここは、人が性質を書き下す領域
- そして、両者をつなぐ層が、最大の未解決問題です
キャリアとして、どう読むか
いま需要が高まっているのはどちらなのか
第６部 ── 世界のどこで求められているのか
- 需要を生む、いちばんの源は「規格」
- なぜ国ごとに需要が違うのか
- 各国間で差が生まれた歴史的背景
- 規格が推奨しても、なぜ求人に直結しないのか
第７部 ── では、あなたはどう位置取るか
- 日本の産業は、この地図のどこに立っているのか
まとめると
第８部 ── では、実際にどう書くのか
- 例１： Lean で「a + b = b + a」を証明する
- 例２： Rocq（旧 Coq）で「リストを2回反転すると元に戻る」を証明する
- 例３： Agda で「空のリストから先頭を取り出せない」を型で保証する
- 例４： TLA+ で「分散システムが不整合な状態に陥らない」ことを検査する
第９部 ── 論理学の理解がどこまで進んだら、定理証明・形式検証を学べ始められるのか
- 目安としては？
- 論理学の教材
第１０部 ── どの言語を、どの順で学ぶか
- その前に ── ５つ全部を学ぶ必要は、ありません
- まず、Lean 4 から
- 次に、目的に応じて分岐する
- Idris 2 の、独自の価値
- 各言語の性格、一覧
- 学ぶ順序、まとめ
- どれくらいの期間を見ればよいか
- 主要な教材
第１１部 ── 学び続けるために
次回予告 ── 各言語のコードを、一行ずつ読む
おわりに ── 需要は、これから広がるか
参考