文字ベースの雑談の難しさ、特に不特定多数の人間が集まる掲示板における雑談の難しさの好例がSlashdot.Japan：あなたが考える「コンピュータ界に最も貢献した人」は？の#1512730にあった。
（next49補足：アラン･チューリングは）基礎も築いたが「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。
# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは
# どういうことなのか…
まず、実際問題として「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」というのは賛成。「バグがなくなったという証明を持ってこいっ」という顧客は無茶な顧客であるというのは全くそのとおり、なのだけれどもこの論の進め方だと脇が甘い。
なぜかといえば、チューリングは「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」ということを直接証明していないため。チューリングがほぼ直接的に証明したのは、#1512749のコメントにあるとおり、「『（任意の）プログラムにバグがないか判定できるプログラム』は存在しない」ということ（ほぼ、直接的にというのは直接証明したの停止性問題）。
なので、元の#1512730の主張は、チューリングが停止性問題を証明したという事実から、「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」というご自身の主張までのギャップもあわせて説明していれば、#1512749のようなツッコミはでなかった。でも、雑談でこういう論の進め方していると言うほうも、聞くほうも面倒なので、あんまり現実的な提案じゃない。
ちなみに、この議論が紛糾するのは#1512749のコメントが微妙に間違っているため。
チューリングの停止性問題は、「（任意の）プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします？
＃「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
計算可能性理論で登場する計算モデル（チューリング機械、λ計算、再帰的関数など）において、計算不可能と判定された問題は、そもそも、それの問題を解く（答えを見つけるか、答えは存在しないことを見つける）有限のステップで終わる手続き（すなわち、アルゴリズム）が存在しないことを示しているので、プログラムが作れないだけでなく、万人がその問題を解くことができないことを示している（個々人の直観や霊感を使えば解けるかもしれない）。なので、お客に「プログラムじゃなくて人間が判定して持ってこい」といわれても困る話。
なので、そこの部分にツッコミが入って議論が紛糾している。で、そのツッコミで展開されているのが「バグがなくなったという証明を持ってこいっ」という点についてなのだけど、これは、ある特定のプログラムに限れば「バグがなくなったという証明」は理論的には用意できる。ただし、バグの定義によって用意する証拠が変わるので難しいけど。
「バグ＝仕様とは異なる振る舞い」ならば、全ての入力に対して仕様どおりに振舞っていることの証拠を見せれば良い。でも、全ての入力がそもそも列挙できなかったり（入力のパターンが無限個ある、時間などの暗黙の入力がある）、平行処理・並列処理を使っていることに由来するタイミング依存の不具合があったり、ハードウェアトラブルがあったり、使っているライブラリやプログラミング言語、コンパイラーのバグ（あるいは仕様）があったり、原因が膨大なので実際的じゃないのは確か。
でも、チューリングの停止性問題の話からスタートしているならば、基本的に理論的なことについて話しているはずなので、計算可能の概念と実現可能の概念は分けて議論されなければならないはず。まあ、雑談なのでしょうがないけど。
下の方のコメントには、ゲーデルの第2不完全性定理が登場したりして、まさにKing of 雑談な様相を見せている。
一番最初のチューリング機械とバグの話についてはこちらのコメントが綺麗にまとめてくださっている。
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
ここだけなんですが、
Xが証明できないならXは存在しないのと同じというのは論理的には間違ってますよね。停止性問題は『「停止性を証明できるチューリングマシン」の不存在』は証明してますけど、
これは、『停止するチューリングマシンがない』というのとは違いますね。
停止するチューリングマシンはありますし。
余談：「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客がいる理由
私の考える答え：発注側の人がプログラムを書いたこと無いため。
情報系の大学卒業者以外で自分から計算可能性理論と計算複雑さ理論を勉強する人は少ないでしょう。でも、日本のIT業界が回っているいるのは、勉強しなくてもプログラムはかけますし、アルゴリズムが思いつかなければ結局どんなプログラムもかけないですし、同じ機能の提供するプログラムを書いたとしても書き方によって天と地ほどの差がでることを経験することが多いので、暗黙に計算可能性理論と計算複雑さ理論を体感するためだと思います（勉強しておいた方が、絶対に自力で高速化を挑戦しちゃいけない問題がわかって便利だと思いますが）。
一方で、発注をする人は、プログラムを全く理解していなくても発注できるのに加えて、たぶん、計算可能性理論と計算複雑さ理論を勉強したことがないと思われるので、無茶なことを無茶と思っていないのでしょう。
