わずか1,919の制御状態を持つチューリングマシン（約100〜200行のPythonプログラムに相当）が、ツェルメロ・フレンケル集合論（ZFC）システムとは数学的に独立した挙動を持つことが示された。これは、比較的規模の小さいソフトウェアであっても、使用するツールに関わらず、現在の数学的枠組みではその正当性を証明できないほどの複雑さに達する可能性があることを示している。
ヒルベルト・プログラムの崩壊
20世紀初頭、数学者のダヴィド・ヒルベルトは、すべての数学を矛盾がなく完全なシステムへと形式化しようと試みた。彼は、形式システムのいかなる性質も、アルゴリズムによって完全に理解され、決定できると信じていた。しかし、この楽観論はクルト・ゲーデルの不完全性定理、およびその後のアロンゾ・チャーチとアラン・チューリングの研究によって打ち砕かれた。
その結果として導き出された停止問題は、コンピュータ科学の最初の主要な定理であり、与えられたプログラムがいつか停止するかどうかを判定できるアルゴリズムは存在しないことを証明した。これにより、一部の計算挙動は本質的に決定不可能であるという根本的な境界が確立された。
「正当性のコストは、エントロピーを減少させるためのエネルギーコストと同様に、計算の『自然法則』の結果であり、回避することは不可能である。」
— Why Writing Correct Software Is Hard
検証の難易度の定量化
ソフトウェアの検証の難易度は、ビジービーバーの定理を通じて測定することができる。この定理は、特定の数の状態を持つ停止するチューリングマシンが実行できる最大ステップ数を表す、計算不可能な関数を定義している。この関数は計算不可能であるため、特定のサイズのすべてのプログラムの挙動を予測できる一般的な「近道」やアルゴリズムは存在しない。
同様に、サイズnのプログラムに対する最小の停止証明の最大サイズも計算不可能である。これは、プログラムの正当性を証明するために必要な労力が、いかなる計算可能な関数よりも速く増大することを意味しており、より優れたエンジニアリングだけでは回避できない「正当性のコスト」を生み出している。
小規模なプログラムと数学的独立性
ソフトウェア検証の限界は単に規模の問題だけではない。それは小規模なプログラムにおいても存在する。ゲーデルの第二不完全性定理を用いて、研究者たちはZFCから「独立」したプログラムを構築した。これらのプログラムは、数学の公理系における矛盾を探索するように設計されている。システムが矛盾を含まない場合、プログラムは決して停止しないが、この事実はシステム自体の中では証明できない。
これらのプログラムは小規模（多くの場合200行未満のコード）であるため、ソフトウェアの挙動が数学的に不定である地点に達する具体的な例となっている。これは、特定の複雑な論理において、限界は計算能力の不足ではなく、数学的な証明可能性の欠如であることを示唆している。
この画像は、記事で議論されているコンピュータ科学と数学の概念的な境界を説明している。
物理的プロセスとしての計算
これらの結果は抽象的な論理に根ざしているが、チャーチ＝チューリングのテーゼを通じて物理世界と結びついている。このテーゼは、物理的プロセスによって行われるいかなる計算も、普遍的な計算モデルによってシミュレートできることを示唆している。したがって、チューリングマシンの理論的限界は、あらゆる物理的なコンピュータの実用的限界に直接反映される。
この図は、抽象的な論理がいかに物理的計算へと変換されるかという議論をサポートしている。
数学をツールとして捉えることと、計算を物理的プロセスとして捉えることの区別は極めて重要である。アルゴリズムは物理世界で実行されるものであるため、計算の「自然法則」は、プログラムが完全な自動的理解や絶対的な正当性と根本的に相容れないことを規定している。