バグのないソフトウェアは作れないと言われますが、正しい命題はちょっと違います。「ソフトウェアにバグがないことは証明できない」です。
バグがないことが証明できない理由は、チューリングマシンの停止性問題が決定不能問題、有限時間内には答えの出ない問題だからです。
えっなんで停止性が有限時間内に判定できないとバグがなくせないの？
等価性判定問題
バグのないことが証明できない理由は、停止性問題の系である「与えられた2つのチューリングマシンが等価であるか否か」判定問題がやはり決定不能問題だからだと説明できます。
バグを定義しましょう。ごく簡単です。「プログラムの仕様と異なる動作」のことです。
バグがないことを証明するとは、仕様という（頭の中にある）チューリングマシンと実装されたプログラムというチューリングマシンの2つを等価判定する問題です。この判定作業には無限に時間がかかるよと証明されてしまっている、それが「バグがないことを証明できない」ことを意味しています。
だから「Hello worldプログラムにはバグがないことを証明できるではないか」という反論がなぜ成立しているのかも容易に理解できます。Hello Worldプログラムはチューリングマシンでなくとも有限オートマトンで記述できる複雑さだからです。つまり、この議論でいうソフトウェアとはチューリングマシンで記述する必要があるプログラム、もう少し具体的にはメモリ要求量が不定なプログラムのことであると理解してください。実用的なソフトウェアのほぼすべてが当てはまるはずです。
仕様と実装が比較し終えられない、だけでなく
実用的なソフトウェアにおいて仕様と実装を完全に比較する（つまり、テストする）のが有限時間内に終わらないと書きました。
で、その仕様というのは一体どんな形で頭の中に、もしくは紙の上にあるのでしょう。
仕様とは、プログラム開始後の入力列からその時点での出力列が得られる関数です。関数と言っても数式で（といいますか有限のルールで演繹的に）完全に表現できてしまうようなプログラムでない限り、入力列から出力列を引ける辞書です。そして、この辞書のサイズが有限ではありえないのです。有限だったらそれ全部試せば有限時間内でテストは終わることになるので。
なんということでしょう、仕様書という辞書はそもそも有限の長さの文書として書き下ろせるものではなかったのです。
完全な仕様書が書けないということは「バグがないこと」どころか「ある動作がバグがどうか判定できる」保証さえないということでもあります。
プログラマの自嘲的な替え歌、「バグは夜ふけ過ぎに 仕様へ変わるだろう」はこうしてみると味わい深い一節ですね。