>>582
そうは言っても普通の数学の証明だって最終的には形式化されないと正しさが確認できないでしょ？
実際に形式化して書くとは言ってないが。

例えて言えば、
　正しいプログラムとはコンパイルして機械語に翻訳できるものである。
　皆が機械語でプログラムを書く必要はない。高級言語で書けば十分である。
　でもコンパイルエラーとなって機械語に落とせないものはダメよ。

ということ。