定理証明器自体の実装が正しいか、という話があったのでついでに：ある定理証明器にはα変換のバグが存在して、6年ぐらい発見されず放置されていたそうです。http://caml.inria.fr/pub/ml-archives/caml-list/2000/10/fd6dcdf412afca28cfae1488e05047aa.en.ht…

http://www.radiumsoftware.com/0707.html#070713全体の是非はさておき（問題自体が古典的＆哲学的で、現時点でこれ以上の抽象的な議論をしても生産的かどうか疑問なので）、Coq云々のあたりはテクニカルな誤解（ないしミスリード？）があるような… Coqなど…