形式手法特論：コンパイラの「正しさ」は証明できるか？ by チェシャ猫

本セッションでは、定理証明支援系 Lean を用いたコンパイラの実装技法を解説します。コンパイラの挙動を保証するための理論的な解説に加え、自作の Lean 製コンパイラで実際に簡単なプログラムをコンパイルして動かす様子もお見せします。

今日、プログラムを書く際に単体テストをつけることは、一種のマナーとして広く普及しています。しかし、かつて Dijkstra は言いました - テストではバグの存在を示すことはできても、不在を示すことはできない。つまり、たとえテストが成功していても、それはたまたまテストケースが不足していた可能性が否定できないのです。

一方、仮に全通りのテストケースを生成してバグの不在を示そうとすると、組み合わせの爆発により膨大な数のテストが必要になってしまいます。例えば「長さ 3 以下の char の配列を受け取る関数」をテストするだけでも入力パターンは 16,843,009 通り、通常の任意長の配列を受け取る関数ならば文字通り「無限個のテストケース」が必要です。

本セッションで紹介する定理証明は、文字通りこの「無限個のテストケース」を扱うための手法です。テストしたい関数の性質を型レベルの制約として表現することで、単体テストのような実行時ではなく静的な型検査時に、かつ「任意の char 配列」のような事実上無限個のテストケースに対して関数の性質を保証できます。

定理証明支援系の中でも、Lean は実際に動くプロダクトが実装できる点で近年人気があり、かの AWS の認可エンジンの検証にも採用されています。本セッションではこの Lean の特徴を活用して、自作言語をコンパイルしてシンプルな CPU 上で動かすための「証明付きコンパイラ」を実装します。

ところで、個別の関数の戻り値ならともかく「コンパイラの正しさ」とは何でしょうか？ 本セッションではこの問題に対して、「ソース言語の意味論」と「ターゲット言語の意味論」の間をつなぐものとしてコンパイラの性質を定式化し、実装したコンパイラが意味論を保存することを証明します。

受講にあたって、定理証明や特定の CPU 命令セットに関する予備知識は要求しません。「コンパイラの正しさとは何か？」に焦点を当て、複雑なプログラムの挙動も数学的にきちんと定式化できるのだ、という感動を味わって頂ければと思います。