全体概要
本セミナーが中心に据える「問い」は、「ソフトウェアとハードウェアの正しさを、どのようにして数学的に保証できるか」というものです。現代のITシステムは社会インフラとして深く浸透しており、航空機・金融・医療・軍事といったあらゆる領域で大規模かつ複雑な分散システムが稼働しています。しかし現状では、そのほとんどのコードは信頼性の数学的チェックを受けていません [p.78]。「テスト・デバッグ・コードレビュー」という開発者中心のサイクルだけでは、潜在的なバグや脆弱性への根本的な対応は不可能であるというのが、本セミナーの出発点となる問題意識です [p.78]。
この問題意識を深掘りするために、第一部では航空機事故（ボーイング737MAXの墜落）[p.16]、分散システムのトラブル（みずほ銀行・ニューヨーク証券取引所）[p.29]、CPUの脆弱性（SpectreとMeltdown）[p.37]、開発コストの高騰 [p.44]、そしてCコンパイラー自身のバグ [p.65] といった現実の問題群が丁寧に提示されます。これらは単なる事故の羅列ではなく、「仕様のバグか実装のバグか」「人間と機械の時間のギャップ」「ツール自体の信頼性」という、ソフトウェア・エンジニアリングの本質的弱点を多角的に照射するための布石です。
第二部では、これらの問題への根本的な応答として「Deep Specification」という新潮流が紹介されます。これは、Coq証明支援システムを中核言語（Lingua Franca）として、ハードウェア・コンパイラー・OSカーネル・ネットワーク・アプリケーションにわたる検証済みコンポーネントを、「豊かで（rich）、二面を持ち（two-sided）、形式的で（formal）、コンピュータで証明可能な（live）」仕様によって結合することを目指す試みです [p.90, p.91]。CertiKOS、CompCert、Kami、Verdiといった具体的なプロジェクトが走っており、単なるアカデミックな理論実験に留まらない実践的な成果を上げています。
第三部では、「形式的手法」の方法論的起源が計算機科学（ホーア、ダイクストラ）と論理学・数学（ハワード、マーチン・レフ）の二つに遡ることが示され [p.182]、20世紀に「プログラム検証は必ず失敗する」と断じた論争の歴史を経て [p.186]、ダイクストラの「証明が与えられているとき、そこからプログラムを導く方が、プログラムから証明を構成するよりはるかに簡単だ」という遺言的洞察 [p.199] が、Deep Specificationの精神的基盤として再確認されます。1980年代に萌芽した形式的手法の夢が、Coqというツールとともに21世紀に復活しつつあるという歴史的位置づけが、本セミナーの大きな結論となっています [p.6]。
—
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: 大規模システム開発の問題
現代の大規模システム開発が内包するリスクを、航空・金融・ハードウェア・コスト・速度・ツールの六つの観点から具体的に提示します。これらの事例は「大規模化・分散化・複雑化」というシステムの構造的変化が、既存の開発手法では対処しきれない本質的な問題を生み出していることを示す証拠として機能しています。「仕様のバグか実装のバグか」という問い [p.21] が、第二部への橋渡しとなります。
■ Part 2: Deep Specificationの世界
第一部の問題群への根本的応答として、「プログラムの正しさを機械がチェックする数学的証明によって保証する」という新しい開発パラダイム「Deep Specification」を紹介します。個別コンポーネントの検証に留まらず、コンポーネント間の仕様を「二面（two-sided）」で接続し、システム全体の正しさを証明可能にするという点が従来の形式的手法との決定的な違いです [p.89, p.96]。
■ Part 3: プログラムと論理
現代の形式的手法の知的系譜を、計算機科学（ホーア・ダイクストラ・ランポート）と論理学・数学（ハワード・マーチン・レフ）という二つの起源から辿ります [p.182]。20世紀の「プログラム検証は必ず失敗する」という論争の歴史を振り返りつつ、ダイクストラの遺言的文書が指し示す原則が、Deep Specificationの精神的基盤と完全に一致することを確認します。