読者です 読者をやめる 読者になる 読者になる

コードが正しいことは証明できない

計算機

不完全性定理や停止性問題に通じる話だと思う.(不完全性と決定不可能性の関係はいまいちよく分かっていない)

その証明が正しいことを証明しろと言われてもできるわけない.説明はできるが,証明はできない.内容見て正しいか判断するしかない.見る人が正しく判断できるというのは仮定だ.

論理が正しいことは論理では証明不可能だ.これは証明できる.

同様にコードが正しいことも証明できない.人間が頑張って読んで正しいか判断する(いわゆるレビュー)か,動かしてみるしかない.動かしてみるというのは機械がコードを読んで判断しているということだ.動かしてみて,動いてるんだから,それで正しいというしかない.

テスト項目があって,合格しているという事実以外何の意味があるのか?合否の結果が正しいというのは信じるしかない.テスト項目に漏れがないことも証明不可能だ.

コードを読むわけでもなく,動かして見るわけでもなく,テスト項目表を見るわけでもない人に,コードが正しいことを証明しろと言われても,それは論理的に無理だ.

論理で論理(コード)が正しいことは証明できない.なんでも理由とか根拠とかを求める論理的な人は,論理を理解していないのだ.*1

そうは言っても,バグってたら困るから,バグを少なくする工夫は当然する.

世界でもっとも強力な9のアルゴリズム

世界でもっとも強力な9のアルゴリズム

*1:というかバグを出すなと言ったらバグがなくなると思える意味が分からない