>>92
CoqはOCaml、AgdaはHaskellで記述されているそうですね。
手元にSMLの入門書があるので、ML→Coqの順に攻略してみようかな。

あと、ちょっと気がついたのですが、
「新しい数学」の提唱者のケメニーとBASIC言語の開発者のケメニーって同一人物ですよね？