お客さんがプログラムを使って、使い終わるまで一回もバグがでないときもあるかもしれませんが、それを前もってなんとか証明できるかどうかです。 もちろん、実際に使って一回もバグが出なかったらそれはそれで結構な話なのですが。 人間だったら前もって知ることができるのでしょうか？

お客さんが欲しいプログラムというのはHello World ではなく、お客さん自身の要求した仕様にあったプログラムなのに、何故かみなさん Hello World の素晴らしさを語っています。

典型的で古典的な勘違いですね。

「あなたのマシンが壊れていて、たまたま VS2008でコンパイルが通ってしまっただけである」のではない証明をしてください。壊れたマシンの上で、たまたまエラーが見当たらないからと言って、障害が無いとはいえない、という点は理解できていると思います。

なお、障害には「ビザンチン障害」というのがあって、ありとあらゆるケースで正しい反応を示すが、唯一あなたが本当に正しく動作してほしい場合にだけ、誤った結果を出す、という障害がありえます。ですので、ビザンチン障害が全く無いことを証明しなくてはいけません。
# 詳細は Andrew S. Tanenbaum 先生の本を読んでくれ。
.

「完璧ではないもの(バグがありえるもの)」の上で実行された結果を使っても、証明にはならないのですよ。それは CPU であっても同じです。チューリングマシンはそもそも CPU というハードウェアとその上で動くソフトウェアをワンセットにしてモデル化したものですから。

ほら～やっぱりわかっていない人がいる。

チューリングの停止性問題は、「（任意の）プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。

それがどうしたのかね?

で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの親コメが「わかってない人」かどうかは判断付きません。

で、手っ取り早く、ツッコミがおかしい事を示そうとすると、反例として「そのプログラムにはバグが無いことを示せる」という事例を挙げることになり、Hello Worldになるわけです。

下記の分析後の個人的な印象ですが、「今の時刻は?」「0時59分」「わかってないなぁ、0時59分42.0034秒だよ」みたいな。調べりゃ分かる/知ってても、普通この流れでいきなりそこまで答えないよね、みたいな所にツッコミ入れてるように見えます。

まず、元コメの議論を追うにはちょっと付け加える必要があって、 (1)「ある計算機Xがあった場合に『X用の任意のプログラムにバグがないか判定できるX上で動作するプログラム』は存在しない」 とする必要があります。

「X用の全てのプログラムにバグがないかを判定できる別の計算機Y用のプログラム」は理論上、存在しえます。 ただしここで言う「別の」ってのは「互換性が無い」程度の意味ではなく、根本的に別次元です。ほとんど反則ですが、夢の計算機Yを「X用のプログラムが与えられたときに、それが正しいかどうかを1クロックで判定する命令」を持っている計算機として考えます。 あくまで数学的な考察なのでやりたい放題です。どんな裏技を使っても良いし、あらゆる既知の物理法則を前提にしても良いからちゃんと動作しそうな具体的なYの設計を考えろ、と言われても多分無理なんじゃないかと。

すると、Yを使うと、(1)の問題が解決出来そう・・・と思いきや、Y自身にも(1)の制限は同じように付いてしまい、 (2)『Y用の任意のプログラムにバグがないか判定できるY上で動作するプログラム』は存在しない」と言うことになります。

じゃあ、と、Y用の全プログラムをチェック出来る、夢のまた夢の計算機Zを定義しても、結局(1)はZに対しても成り立つので、(3)『Z用の任意のプログラムにバグがないか判定できるZ上で動作するプログラム』は存在しない」。以下、(4)、(5)、・・・と、どこまで行っても、「あらゆるプログラムのバグを見つけられる存在は存在しない」と言うところに落ち着きます。

んでまあ、実用上、(1)だけ考えていれば困ることはないんです。なにせ、計算機Yの時点で具体的に想像する事すらほぼ不可能、そんな物が目の前に現れるわけがないんですから。世の中で使われてる計算機は全てX互換機と仮定してOK、ぐらいの勢いです(正確にはXの劣化版。量子コンピュータですらこの範疇に含まれる)。

更にツリーを遡ると元コメの親コメの親コメ [srad.jp]は、「バグ無しを証明しろと言われて困る」だったので、上記を当てはめると「証明しろ」「計算機Xでは不可能です」「いいや、計算機Yがあれば出来るだろう」「計算機Yが正しいかどうか・・・」「計算機Zを使え!!」という、相当マニアックな顧客と言うことになりますね。 普通は「いやいや、計算機Yなんて実装できませんし」となるかと。

ついでに、元コメのどこが意地悪かというと、

そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。
p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…
p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着してしまう。

この辺も、非常にミスリードです。「プログラム」=「計算機の定義(設計)+その上で動作するプログラム」と言う 意味で書かれていて、このp1、p2が、上記Y、Zに相当するわけです。バグ取りの実務でよもや計算機Yが話題に上るとは想像出来ず、「プログラムp0、p1、p2、・・・」を「計算機X上で動くプログラムp0、p1、p2」をとして読み進めてしまい、釣られてしまったわけです。

元コメは、分かってない人用の説明っぽく書きだしておいて、その実、ちゃんと分かってる人でないと、 言わんとすることが分からない説明ですね。

# 以上、自分がこのジャンルに自信がないので、間違った理解をしていないかチェックの流れ。
# 「良くある間違いはコレだ!」と、表題が付いてるのはチェックに最適なもので。

ここでの話題って、#1512749から分岐して誘導されていると思うんですよ

• 「任意の」を前提にした主張に対して反証は「特定の」としてhello worldがありますよっていう話
• 「任意の」はおいといて、装置を移動した場合の議論

で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。
残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。
プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させたうえで問題を単純化し、特殊事例としての「バグのないプログラム」問題に変化させて解決しようとしている。←ここでチェーンを終了させてようとしている、というか次のチェーンがないので仕方がないんですけど。
「計算機Zを使え!!」は現場では「次の計算機はSEだ」で、「次の計算機は顧客だ」になるようにしている。
それでバグがないことを（常に）証明できるか？というとそうではなくて、証明できるケースもあるだろうし、できないケースもある。人間が納得できるレベルまで不完全性を縮小できればいい、ということまでしか言うつもりはないんですけど。

そういう矮小化された議論が成り立たないような問題を解く領域では、バグがないことを保証することはできないような逆の意味のHello Worldを出すことも可能ではあるわけですが。

私の認識では、「人間が解決済みの課題を処理させるためのプログラム」なら、判定装置を人間側に誘導することが可能で、「人間が解決していない課題をプログラムに代わって解かせるためのプログラム」については判定装置の移動で問題を先延ばしにしても収束しない、と思っています。

そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。

は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。

この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確かめておく、という手順とは言わば逆のやり方になるわけですが。

要するに『p0は信用出来るのか?』という疑問は、p0が『xは正しい』『xは間違っている』としか出力してくれない場合にだけ起こります。p0が、『xは、(1)再帰を含めて全てのループは有限回で止まる。なぜならループ変数iは・・・・(以下xの中身を引用した数学的証明)、(2)答えは仕様通りになる。なぜなら(同様に証明)。よってxは正しい』と、出力してくれれば、p0の信頼性は気にしなくても大丈夫です。その出力をSEなり顧客なりが読んで、筋が通ってるかどうかだけ気にすれば良いんで、p1、p2、・・・の出てくる余地はありません。

ちなみに、この場合のp0は「ある特定の構造をしたプログラムのみ解析出来る」とかそんな物になります。 その構造をしてないxを与えた場合には「このプログラムは分からない」とでも出力します。 似たようなのは売ってます。ただ、出力される「証明」が非人間的な記述方法と量になるので、 その「証明」を読み解くことは事実上不可能ですが。 よって、おおむね、「p0は正しい」というのを信じるしか無いわけです。

こういう方法で、1ターンで事を「プログラムの正さの証明」から「数学的に記述された証明」に落とせるので、私としては「筋が通ってても、『数学が正しい』という保証がないから無駄」と言う意味かと最初に誤解しました。 私がコメントを付けた最初のコメントは、「正しい/間違ってる、としか出力しないプログラムだと、どうやってオーソライズする? 読み解けないほど長い証明を出しても無意味」という主張だったんですね。停止問題を理解してるかどうかとは無関係な議題ですね。

間違い。

p0 がxについての評価結果を出したとしよう。
その評価結果が正しいということを「どうやって証明するのだね?」

いいかい?ここでいう「証明」というのは意外と厄介な存在だ。たとえば、

while(1);

という記述があるとする。これゆえにp0は「無限ループになっています」と出力したとしよう。キミも私もそれに同意したとする。それでは証明とはいえない。p0とキミと私がバグっているだけかもしれないではないか。

ちょっと世界中の技術者と計算機科学者全員に問い合わせてみる。全員 p0 の出力に同意したとする。それでは証明とはいえない。

K&R に「while(1); と書いたら無限ループになります」と書いてあったとしよう。それでも証明とはいえない。

有限の帰納的蓄積は証明とは言わない。機能的蓄積が使いたければ、帰納法を使って無限を扱わなくてはいけない。

それを漠然としたイメージって言ってしまうと、もともこもないんでは？

無限ループとは何かを、公理から導いて定義したうえで（じゃないと命題にならんので）、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。

いや、それでも、その証明が正しいことをどうやって証明する？なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。
その証明を否定するには、「それをどうやって証明する？」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。