関数型言語マニアのための論文紹介６：定理証明器で書かれたCコンパイラ

Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Xavier Leroy. POPL 2006.

著者のXavier LeroyはOCamlの作者です。

（ネイティブコードを吐く）コンパイラを作ったことがある人なら、ごく稀にしか起きない、わけのわからないバグに悩まされたことがきっとあると思います。そういうバグがあると、コンパイラを作る人どころか、それを使うプログラマも悩まされます。これはMLのような型つき言語でコンパイラを書いても（少しは楽になりますが）おいそれと解決する問題ではありません。MLの型は、たとえば「入力が整数なら出力も整数である」「入力がリストなら出力はboolになる」といった単純な性質しか表現できず、「コンパイルした結果がソースコードと等価である」といった高度な性質まで検証できないためです。

そこで、（非専門家むけのいい加減な説明ですが）MLのような型をもっともっともっと強力にして、ある種の論理で表せる性質はすべて記述・検証できるようにした、たとえばCoqのようなシステムがあります。このようなシステムは普通は「定理証明器」といわれますが、すごく強力な型(dependent type)を持ったプログラミング言語とみなすこともできます。

そういう「強力なプログラミング言語」でCコンパイラを記述して、バグがない（コンパイラの出力するPowerPCのアセンブリが、Cのソースコードと等価である）ことを証明してしまった、という研究です。この論文ではCのサブセットしか扱っていませんが（それでもすごいですが）、範囲をどんどん拡張する計画も進行しているようです。

定理証明が本職の人々にいろいろと突っ込まれそうな書き方になってしまいましたが、素人ということで大目にみてください…。そういう方にはPOPLmarkという研究のための練習問題も公開されているので宜しく、とついでに宣伝。