「バグのないプログラム」と「バグのないプログラムは作れない」と停止性問題について

停止性問題やライスの定理を持ち出して、「バグのないプログラムは存在しない」もしくは「バグのないプログラムを作ることができない」という主張が、数学や論理に長けた人の間でも交わされることがあります。
いやいやそんなことはないよ、という話をするんですが、そうすると決まって、「君は停止性問題を知らないのか?」という初歩的なツッコミが入る確率95%・・・

停止性問題について

簡単に書くと、停止性判定問題とは任意のプログラム*1が無限ループするかどうかを別のプログラムによって判定可能かどうかという問題。ちなみに、これは判定不能であることが証明されています。*2
Wikipediaの説明は微妙なんですが、こちらの補足がわかりやすいです。

なぜミスリードするのか

すでに証明済みの定理を用いて"論理っぽい言葉でつなげる"と、比喩的に似ていればいるほど、あたかもそれが正しいかのように錯覚してしまいます。そして、錯覚してしまう人が多いという事実を前にして、錯覚していない人までが他者の錯覚を利用してしまうわけです。それは悪意というレベルでないとすれば、ちょっとした知の悪戯のようなものかもしれませんが。

証明のレイヤーをずらすのはどうなんよ

停止性問題そのものは固いです。証明のレイヤーを外して、チューリングマシンじゃなくてノイマン型だったらどうかとか、プログラムじゃなくて人間という装置だったらどうかとか、最初から有限のステップ数を決めておいて、そのステップに達したら終了するようにしたらどうかとか、そういう次元をずらした各種バリエーションがあるわけですが、いずれにしても停止性問題が揺らぐわけではありません。
逆に、証明できたとして、その証明の正しさはどうやって証明する?という連鎖を持ち出す人もいるようですが、これもまたレイヤーをずらしているだけです。
一方で、「実務上は証明できなければ、存在しないのと同じ」という論法もいかがなものかと思います。実務上の話のような個別事情を持ち出して、証明のレイヤーを外れるならそんな「証明くさい」表現は避ければいいと思います。
ただ、机上の空論をやるわけじゃないんで、実務上の話も最後の方で言及しておきます。

悪魔の証明

人によっては存在しないことを証明することは、存在を示すことよりも難しいという悪魔の証明を持ち出して、非常に人間くさい表現によって、可能不可能を論じたがるようです。そういう思春期的発想には、私はもう若くはないのでついていけません。

証明っぽく

「バグ」とはバズワードであって厳密ではないのでここでは限定して問題を定義しなおしてみます。
バグのないプログラムを下記のようなものと仮定して進めてみます。それ以外の事象についてはここでは扱いません。

  • あるプログラムが、正常終了すること
  • あるプログラムが、定められたそれらの入力について出力が仕様を満たしていること

ライスの定理

仕様を満たすかどうかというと、ライスの定理でしょうか。プログラムが満たすべき自明でない任意の性質を別の検証用のプログラムによって判定することはできない、ということも証明されています。
それでは、停止性問題の決定不能性定理とライスの定理をもって、「バグのないプログラムは存在しない」と言えるでしょうか。

バグのないプログラムは作れない ?

これは少し言い変えてみると、
バグのないプログラムは作れない => 作られたすべてのプログラムにはバグがある
ということになります。これ、たとえば停止性問題で、「作られたすべてのプログラムにはバグがある」が正しいと仮定すると、すべてのプログラムは停止しないというのと等価になります。すべての入力に対して「停止しない」と決定するプログラムがあればよいことになりますので、停止性問題の決定不能性定理と矛盾します。
つまり、論拠とした停止性問題によって、「バグのないプログラムは作れない」は容易に否定可能なわけです。

実務上はどうか

それでは、実務上はどうか。
実務とは個人的なものであって、客観性のかけらもないレイヤーなので問題にするべきレベルではないような気がするのですが、乗りかかった話なので・・・
「バグのないプログラムは作れない」と公言してしまうタイプの人は、

  • これまで正常終了するプログラムを書いたことがない
  • 正常終了して想定した動作をしていても、それを信用しない。

のいずれかなんでしょうが、まぁ、後者の可能性が高いでしょうか。
また、実務上というのは難しい≒作れない、であるし、その難しいという個人的感覚に基づいて言えばどちらにでも取れてしまうわけです。実際、実務上、バグがないことを証明しろと言われれば、「現状でそれは無理」もしくは、「証明費用が開発費用の数倍かかり、なおかつ、厳密な証明ではなく近似的なものになりますよ」という話をすると思います。それはすなわち実務上は限りなく不可能に近いと言ってもいいかもしれません。でも、その話はあくまでも実工数が膨大で時には不可能なこともありうるのでという意味で無理という表現をするわけですが、その論拠に「停止性問題」が使えないのは上記した通りです。
単純な話です。性能を判定するプログラムを書くのは難しいんですわ。ただそれだけ。
結論や言動は似ています。 そこで説得するために、ミスリード覚悟で欺瞞的に「停止性問題」を持ち出すことを卑怯だと感じるか、目的に対して手段を選ばないのか、そういう違いでしょうか。
最近では、TDDが普通になってきて、テストを書いてから実装するという手順によってプログラムのバグを減らす努力がなされていますが、実際に完璧なテストを書くというのは無理があります。が、それは書かない場合よりも何倍もマシであろうということは言えます。実務上は、バグを検証するために有効とされているあらゆる手段を使って、バグを減らすための努力をしているかどうかというのが重要なわけです。

困ったチャン

ところが、困ったことに、数学的な話が好きな輩は、「停止性問題」を持ち出して酒の肴にするためにこういうことを言っているようです。つまるところ与太話ですね。この与太話をできるレベルの人っていうのは、ネタとして認識しながら話をしているわけですが、サイエンス的に周囲の信頼を集めていたりするので、本人は与太話のつもりで話しているのにそれを聞いた周りの人が、それを本気にしてしまう。するとそういう言説が一人歩きしてしまうんですね。
これちょっと、新型インフルエンザのマスク論争に似ていたりw

それでも残る課題

ライスの定理で注目されるのは、性能が自明な場合を除いて、プログラムの性能をプログラムで証明することはできないという部分の、「自明な場合」です。これ、やわらかく(わかりにくく)言うと、入力に対する出力への関係が既に証明済みの型*3にプログラムされていて正常に動作することが保証されている場合と言えると思います。これは、ライスの定理に反しません。
果たして、それを認める立場をとるかどうかが、この与太話のオチになりそうです。

あぁ、ちなみに、これは与太話!

*1:チューリングマシンの想定

*2:ここではやわらかい話なので、不完全性定理とかライスの定理とかに踏み込む必要はないかな。

*3:一般には、その自明部分はカリーハワード対応などによって示すと思います。Haskellベースのagda2はその実装か