social process

http://www.radiumsoftware.com/0707.html#070713

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

• Coqなどの定理証明器は（論理学としての）いわゆる型理論にもとづいていて、（通常は）人手による証明より、Coqによる証明のほうが信頼できると認知されている
• 一般に定理証明器によるプログラム検証では、「紙面」はあくまで単なる「解説」に過ぎず、数学的／形式的証明は定理証明器だけで完結している（Coqなどの定理証明器が信頼できると仮定すれば、ユーザは証明の中身ではなく、定理のステートメントだけ確認すればOK）

あと、平方根は特にややこしい数学的なプログラムの例で、普通のプログラムはもうちょっと簡単なことも多いのではないかと思います。（追記：定理証明器によるプログラム検証が直ちに広く実用になる、というわけではありません。たとえば今のCoqでMinCamlを検証しようと思ったら一大プロジェクトになってしまいます…）