(はてぶ)バグのないプログラムを書くことは理論上は可能である - shi3zの長文日記

[ バグのないプログラムを書くことは理論上は可能である - shi3zの長文日記] プログラムのわからないえらい人「バグのないプログラムを書くことはできないのか?難しいかもしれないが、十分に気を付けていれば防げるのではないか?」にどう返したらいいのかわからない http://anond.hatelabo.jp/20170214114736 バグのないプログラムを書くことは理論上は可能である。 そのためのツールもノウハウもある。 それを定理証明支援系言語と呼ぶ。 定理証明支援システムまたは自動証明器のためのツールとしてはCoqやAgdaが有名 Coq - Wikipedia Agda - ...
b.hatena.ne.jp/entry/d.hatena.ne.jp/shi3z/20170216/1487200968 :

単純に、出版社みたいに、校正に人を入れれば、バグはぐっとなくなるってだけでは。そんなに高度なことじゃない。もともと、一人だけでコードを書いて動作チェックもする歴史だから、大先生は、後からコードを読んでもわかるように、文芸的にコメントをつけるとか、構成をわかりやくして、作業をするとかという歴史があるんだよね。

 

ま、だいたい、バグって、くだらないループの抜け方が悪いとかばかりだと思う。あとは、ゼロからはじまるのに、イチからはじまると勘違いしたり。