１行でできるCoqプログラム

次の１行を書いて、〜.vというファイルを作ってみよう。

Extraction "plus.ml" plus.

これであなたも立派なコカーだ！じゃあ早速コンパイルしてみよう。

/yoshihiro$ coqc 〜.v

これで、plusという名前のCoqにもともと用意されている足し算関数がOCamlに変換されて、"plus.ml" というファイルが作られるのだ。
現在のフォルダを見てみよう。"plus.ml"というファイルが新たにできていることが確認できるだろう。
「Coqなんか使わなくても足し算なんか今時どんなプログラムでもできるよ。」という意見もあるだろう。だが、その人はその足し算のコードを見たことがあるのだろうか？
おそらく多くのプログラマは足し算などの基本的な関数を検証すること無しに、使っているのではないだろうか。
「今まで問題なかったのだから大丈夫。」と心の中で思っているのではないだろうか。
Coqで作ったこの足し算関数は、スタンダードライブラリにある多くの定理によって、その基本的な性質が証明されている。
この足し算が可換であるとかモノイドを生成するとかいった性質は、もはや疑いの無い事実として証明されているのだ。
これほどまで正しさを保証された足し算を使ったことがある人はどれだけいるだろうか？
足し算だけじゃない。かけ算もリスト上のマップ関数も同様のやり方で、簡単に得ることができる。
さらに自分で証明をすれば、今作ったばっかりの関数もテスト無しで、安心して使うことができるのだ。
今日のまとめ

1. 1. ずっと使われていたプログラムにもミスが無いとはいえない
   2. 証明さえすれば、テストをする必要も無く、正しさが保証される。