停止性問題は決定不能→バグのないソフトウェアは作れない？

「チューリングマシンの停止性問題が決定不能だから、バグのないソフトウェアは作れない」という説を（アカデミックな人からも）よく聞く*1のですが、（結論はともかく）論理が理解できません。「停止性問題が決定不能 → Completeな自動検証器は実装不能 → バグのないソフトウェアは作れない」の２番目の矢印が成り立たないと思うのですが、別の意味？（もちろん、今のCoqやCharityですべての業務プログラムを記述しろ:-)とか言うつもりはありませんが）

P.S. bonotakeさんからコメントをいただきましたが他の方のために：「Completeな」（バグがあれば必ずyesと答え、バグがなければ必ずnoと答える）という限定条件もついているので注意が必要です。バグの種類にもよりますが、単にsound（バグがあればyesと答える＝noと答えたらバグはない）とか、「十分に近似」とかであれば、実装可能な（それなりに有用な自動検証器が実在する）場合も少なくありません。メモリ安全性に対する（強い）静的型システムとか、Coverityとか、Terminator（停止性検証器そのもの）とか。またどこかのレポート課題の解答になっているかもしれませんが、自分で理解せずに写したら必ずバレますので学生さんはご注意を…:-)

P.P.S. ここ↑でいう（検証が）「健全(sound)」とは、「もし本当にバグがあったら、バグがあるよーと教えてくれる」という意味です。「完全(complete)」とは、さらに「もしバグがあるよーと言われたら、本当にバグがある」という意味です。例えば（強い）静的型システムはメモリ安全性に関して健全ですが、完全ではありません（普通は）。コンパイル時エラーが出ても、（仮に実行できたとして）必ず実行時エラーが出るとは限らないためです（無限ループの「後」でエラーを起こすプログラムとか）。よそで質問されたので補足でした。

ついでに、「チューリングマシンの停止性問題が決定不能」というのは、次のような（チューリングマシンの）プログラムHが存在しない、という定理です。

Hは任意のプログラムPと任意のデータXの組(P,X)を入力として受け取る。もしPにXを入力して実行したら停止する場合、Hは「yes」と答えて停止する。そうでない場合、Hは「no」と答えて停止する。

細かいことを抜きにすれば証明は簡単で、典型的な対角線論法です。（学部１年生のときに一般教養の授業で習った「証明」の受け売りです。）

上述のようなHが存在したとする。「任意のXについて、Xを入力として受け取ったらH(X,X)を実行し、答えがyesだったら無限ループ、noだったら停止するプログラム」をDとする。D(D)が停止するかどうかで場合わけする。もしD(D)が停止するならば、H(D,D)はnoを返したはずなので、Hの定義よりD(D)は停止せず矛盾。もしD(D)が停止しないならば、H(D,D)はyesを返したはずなので、Hの定義よりD(D)は停止してやはり矛盾。

「細かいこと」は抜きにしているので、プログラムや組を入力として表す方法（エンコーディング）の詳細とかはご容赦ください。:-)

*1:新聞記事のインタビューに書かれていたこともあります。新聞なので、本当にそう言ったのかどうかわかりませんが