講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「IT技術とCoqの世界」は、「証明＝プログラム＝計算」という三項同値という深遠な命題を出発点として、コンピュータの論理的・数学的推論能力が現代のソフトウェア開発をどのように変革し得るかを探求するものです [p.1]。
現在、ほとんどのエンジニアにとって機械によるチェックつき数学的証明は学術的な好奇心の対象に過ぎず、テストやデバッグ、コードレビューといった人間中心の開発サイクルが当然の前提とされています [p.2]。しかしAdamChlipalaが「Coming Soon」と宣言したように、この状況は変わりつつあります [p.3]。
セミナーは二部構成を取ります。第一部「開発の世界を考える」では、なぜ開発が人間によって担われているのかという根本的な問いから始まり、仕様と実装の関係が本質的に論理的であることを示します。そして「証明＝計算」（チャーチ＝チューリングのテーゼ、1930年代）と「証明＝プログラム」（カリー＝ハワード対応、1970年代）という二つの歴史的発見を辿ることで、コンピュータが形式的証明を実行できるという認識がどのように形成されてきたかを明らかにします [p.51]。
第二部「Coqの世界」では、証明支援システムCoqとの対話的証明構築を体験しながら、Coqが人間と機械の協働によって仕様の正しさを形式的に保証する道具となっていることを具体的な実例で示します。スタックマシンの仕様記述とコンパイラの正当性証明 [p.133-145]、さらにRISC-Vチップ設計プロジェクト「Kami」 [p.155-169] を通じて、Deep Specificationという思想仕様は動作するプログラムであり、実装の正しさは形式的に証明できるが実用段階に入りつつあることが示されます。
本セミナーの核心的なメッセージは、計算に関して人間とコンピュータに本質的な差はなく、ラムダ計算もチューリングマシンも人間の計算の忠実なモデルに過ぎないという認識です。Coqの実践的経験こそが「計算＝証明」「証明＝プログラム」というミッシングリングを埋め、機械が論理的・数学的推論能力を持つという直感を開発者にもたらすと筆者は訴えます [p.77]。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: 開発の世界を考える
現代のITビジネスにおいてソフトウェア開発がなぜ人間中心の複雑な構造を持つのかを解析し、テスト・デバッグ・コードレビューの反復サイクルが「仕様と実装の論理的関係」を人間が担っているためであることを明確にします。そのうえで、コンピュータが論理的推論能力を持てばこの構造が根本から変革できるという展望を、歴史的・理論的根拠とともに提示します [p.9, p.33-38]。
■ Part 2: Coqの世界
Coqとの対話的証明構築を疑似体験させることで、人間がtacticという「戦略的命令」をCoqに与え、Coqが「証明の状態（仮説とサブゴール）」を返すという協働プロセスを体感させます。続いて実際の仕様記述例スタックマシンとKamiプロジェクトを通じて、Coqによる形式的仕様が「動作するプログラム」であり実装の正しさを証明できることを具体的に示します [p.84-85]。
ページのナビゲート