#27 形式手法ってなに？——"数学で仕様を書く"ただの道具の話

くわラジ · Nov 5, 2026 · 35m

形式手法（フォーマルメソッド）とは何か？ 日本語で書いた仕様書はなぜ「顧客が本当に欲しかったもの」とズレるのか——数学を土台に仕様を書き、解釈のブレをなくすという形式手法の考え方を、入門としてざっくり解説する回です。

「形式手法がまったく分かってない」と言うへんてこに、kuniwak が動物園や三角形の面積のたとえで、形式言語・数学基礎論・定理証明支援系とのつながりを噛み砕いていきます。後半は、AI に TLA+ や Lean で後から検証させる「バイブ形式手法」の落とし穴を取り上げます。テストとの違いである「有限の壁」や、"何が保証されていて何が保証されていないか" を人間が把握すべき理由も話しています。数学が苦手でも「道具として使えればいい」と思える、形式手法シリーズの第1回です。

▼チャプター

00:00 オープニング

00:12 形式手法の定義と「形式」の意味

08:08 数学基礎論と論理的検証

14:25 形式手法における理学と工学の側面

19:06 バイブ形式手法の注意点

30:18 実装先行の課題と設計段階での活用

33:33 エンディング

▼この回で話していること

・形式手法とは？「形式」の意味と、数学で仕様を書く理由

・自然言語の仕様書（PRD など）が曖昧になる問題

・プログラミング言語も形式言語の仲間という話…