正しいソフトウェアを書くのが難しいのはなぜか：計算理論が示す本質的な限界
Why Writing Correct Software Is Hard
プログラムの正しさを完全に理解することは、計算理論の観点から根本的に不可能である。停止性問題やRiceの定理、ビジー・ビーバー関数の非計算可能性は、いかなるツールを使っても正しさの保証には大きなコストが伴うことを示す。さらに、ZFCから独立した小規模なプログラムが存在し、その振る舞いは数学的に決定できない。
数学者にとって「我々は知らないし、知ることはない」ということはない。……解けない問題が見つからない本当の理由は、解けない問題が存在しないからだ。愚かな「知ることはない」に対して、我々の信条はこうだ：我々は知らねばならない、我々は知るだろう！
HNでの議論
143- turbobutton
ソフトウェアにおける抽象的で数学的な正しさと、現実世界での機能性との間には厳然たる区別があると思う。入力を処理し、人間に複雑なワークフローを提供するあらゆるソフトウェアは、必然的に現実の果てしない気まぐれに対処しなければならない。
だからといって形式的な正しさに価値がないわけではないが、重要なのはそれがいつ役に立つか、いつ手間の方が大きくなるかを見極めることだ…
- mpweiher
まず「正しい」とは一体何なのかをはっきりさせないといけないと思う。
形式的仕様に対して正しいということ？
その仕様が「正しい」とどうやって分かるの？定義によるの？
- johnbender
私の理解では、この記事はライスの定理と、YedidiyaとAaronsonが生成した小さなプログラムについて何かを証明できないという考えを誤って混同している。しかしライスの定理が教えてくれるのはそういうことではない。代わりに教えてくれるのは、あるプログラムが与えられた地点に到達するかどうかをすべてのプログラムについて正しくイエスかノーか判定する一般的な方法は存在しないということだ。
特定のプログラムと一度きりの証明であれば、多くのことを証明できる。あるいはループが停止すると仮定して過大近似すれば、時には正しいプログラムを拒否するリスクを負いつつも、多くのことを健全に証明できる（例えば型システムのように）。
これは言語の癖か、私の解釈の問題かもしれないが。
- kodoman
形式的検証にはずっと興味があったが、書いたのはおもちゃの証明と導出プログラムだけだ。
「AIがリーンする」とか、形式的検証は簡単だ、あるいはAIにとって簡単になるだろうから脳のスイッチを切っておけばいいという前提の外で、この話題の古い議論が見られるのはいいね。
そもそも検証可能なプログラムを構築するのは難しい設計問題で、本当の思考と問題への深い洞察を必要とする。
- tromp
> 1919個の制御状態を持つチューリングマシンで、停止することを証明できない（つまり「ZFCから独立」）。このマシンはとても小さく、4Kチャレンジに余裕で収まる
小さな揚げ足取りを一つ：
4Kチャレンジは通常4KBに収まるコードを指すが、1919状態のTMを素直にエンコードすると19192(2+11) = 49894ビット、つまり6237バイトで6KBを超える。
しかし最近のAIによる最適化で状態数は最大215まで減り、1KBに余裕で収まる…
- nirinor
否定的な主張で最も重要な部分は暗黙のうちにある：どのような合理的な仮定があればその主張を否定できるか？
確かにライスの定理により、任意の関数が常に2つの入力の和を計算するかどうかを判定できるプログラムは存在しない。しかしそれは、和関数の解析が極端に難しい実装を許しているからに過ぎない。したがってこの定理は、和の単純な実装が正しいと証明できるという事実と共存する。
この観点から、最良の結論は「合理的な時間で正しいソフトウェアを書くには、解析しやすい言語とプログラミングスタイルを使わなければならない」だと思う。
- bluGill
本当の疑問は：典型的なプログラムについて、証明できないプログラムがあると知っていても、それを証明できるのか？
与えられた例には興味がない。興味があるのは自分のワープロやウェブブラウザなどだ。スクリプト言語に制限を設けることで、それらを証明できるのか？
- myrmidon
BB(6)チャンピオン（2記号6状態のビジービーバー）の下限が記事の古さを示しているのが興味深い：記事では>10^36534とあるが、現在のチャンピオン（mxdys 2025）は>10↑↑10↑↑10↑↑8だ（10↑↑8は10^10^10^10...と8段のべき塔で、式は右から左に評価されるので、10↑↑10↑↑8はすでに完全に想像を絶する大きさだ）。