LEAN自身の正しさはどう証明するの。それがC言語で書かれていたら、
そのプログラムの正しさをどうやって証明するのかな。
かりにC言語で書かれたプログラムが正しくても、それをコンパイル
して生成された機械語プログラムが正しいものになるためには、
コンパイラの正しさと、機械語をCPUや計算機のハードとOSが
正しく実行することが必要。I社のCPUはエラッタが多いぞ。
コンパイラも頻繁にバージョンアップがあるということは
バグも多いだろうし、バージョンが上がればバグが減ること
は保証されない。OSもWindowsなどバグだらけだろう。
Linuxだってカーネルやライブラリやデバイスドライバも
含めてバグはある。また長時間計算すると、電気ノイズや
宇宙線などの影響により正しく計算できる確率は時間と
ともに指数関数的に減少する。ECCも無いようなメモリを
使っている安物のPCによる計算結果は信用するに値しない。