2010-08-06 そうだ目標は・・・ ocaml coq coqだった。あまりにアホナ間違いを繰り返す自分に嫌気がさして、定理的にプログラムを定義して、後から変換もできる、というのに惹かれたんだった。今晩当たり勉強できるかな・・・