一个仅包含1,919个控制状态的图灵机——大致相当于一个100到200行的Python程序——已被证明拥有在数学上独立于策梅洛-弗兰克尔集合论（ZFC）系统的行为。这表明，即使是相对较小的软件片段，也能达到一种复杂度水平，无论使用何种工具，其正确性都无法通过当前的数学框架来证明。
希尔伯特计划的崩溃
在20世纪早期，数学家大卫·希尔伯特试图将所有数学形式化为一个一致且完整的系统。他相信任何形式系统的属性都可以通过算法完全理解和判定。这种乐观态度被库尔特·哥德尔的不完备性定理以及随后阿隆佐·丘奇和艾伦·图灵的工作所瓦解。
由此产生的停机定理——计算机科学的第一大定理——证明了没有任何算法能够判定给定的程序是否会停止。这建立了一个基本边界：某些计算行为本质上是不可判定的。
“正确性的成本——就像降低熵的能量成本一样——是计算‘自然法则’的结果，这是不可能避免的。”
— Why Writing Correct Software Is Hard
量化验证的难度
软件验证的难度可以通过“忙碌海狸”定理来衡量。该定理定义了一个非可计算函数，代表具有特定数量状态的停机图灵机所能执行的最大步数。由于该函数是非可计算的，因此不存在任何通用的“捷径”或算法可以预测所有特定规模程序的行为。
同样，大小为n的程序的最小终止证明的最大尺寸也是不可计算的。这意味着证明程序正确性所需的努力增长速度快于任何可计算函数，从而产生了一种无法仅通过更好的工程手段来绕过的“正确性成本”。
小型程序与数学独立性
软件验证的局限性不仅仅是规模问题；它们甚至存在于小型程序中。利用哥德尔的第二不完备性定理，研究人员构建了在数学上独立于ZFC系统的程序。这些程序旨在寻找数学公理中的矛盾；如果系统是一致的，程序就永远不会停止，但这一事实本身无法在系统内部被证明。
由于这些程序很小——通常少于200行代码——它们成为了软件如何达到其行为在数学上无法确定的具体例子。这表明对于某些复杂的逻辑，限制不在于缺乏计算能力，而在于缺乏数学上的可证明性。
这张图片展示了文章中讨论的计算机科学与数学之间的概念边界。
计算作为一种物理过程
虽然这些结果植根于抽象逻辑，但它们通过丘奇-图灵论题与物理世界联系在一起。该论题表明，任何由物理过程执行的计算都可以由通用计算模型来模拟。因此，图灵机的理论极限直接转化为任何物理计算机的实际极限。
此图表支持关于抽象逻辑如何转化为物理计算的讨论。
将作为工具的数学与作为物理过程的计算区分开来至关重要。因为算法是物理世界中执行的内容，计算的“自然法则”决定了程序在本质上与完全的自动化理解和绝对正确性相冲突。