Why Writing Correct Software Is Hard
编写正确的软件之所以从根本上存在难度，是因为计算本身的性质带来了不可避免的限制。以 Gödel 、 Church 和 Turing 的奠基性工作为根源的理论计算机科学表明：我们无法完全理解或预测任意程序的行为。 Halting theorem 证明不存在任何算法能够判断一个程序最终是否会终止，其推论（如 Rice's theorem）也说明，判定程序行为的任何非平凡性质同样是不可能的。这些结论意味着，程序本身与实现完美正确性所需要的那种完整理解在本质上是彼此冲突的。
计算复杂度则让这些限制更具现实意义。仅仅"在理论上可判定"还不够——如果求解一个问题所需要的资源超出了合理范围，那就难以落到可用的工程方案上。即便问题在技术上能够解决，完成它所需的时间和精力也常常会增长到现实中难以承受的程度。正如 Juris Hartmanis 和 Richard Stearns 等研究者所指出的，复杂度就像自然法则一样客观存在。相关结果表明，我们不可能比程序自身的运行更快地分析出它的行为。因此，将验证视为一种决策问题，它在计算机科学中属于最棘手的挑战之一；正确性也不可能简单地拆分成若干模块化、可管理的部分。
编程语言中的抽象机制——例如高层结构、函数以及并发——并不能神奇地绕开这些核心困难。尽管这些特性让人更容易编写程序，但它们并不会以某种方式简化底层状态空间，从而让验证在一般情况下变得可行。即使在理论上可以进行验证的有限状态机场景中，该问题往往也属于 PSPACE-complete 。这意味着，用更简洁方式表示的程序未必比更冗长的版本更容易验证。对于自动化模型检测器而言，状态爆炸仍然是一个重大障碍：它们必须面对真实软件中庞大且常常不规则的复杂性。
各种验证方法——包括模型检测、演绎证明和静态分析——都必须在这些固有的边界内运作。诸如抽象解释或类型系统之类的技术，往往通过牺牲精确性来换取可操作性，从而给出可靠但不完整的结论。它们确实能帮助发现某些类别的缺陷，但却无法保证所有程序的完全正确性。试图为软件可靠性寻找一种"一劳永逸"的通用方案，本质上近乎现代炼金术。正如 Fred Brooks 所强调的那样，软件工程中不存在"银弹"，我们必须接受：复杂度正是我们所构建系统的本质特征。
从最终的现实出发，最可行的方向是采取一种类似自然科学的经验主义和临场应对。既然无法验证所有程序，就应该研究人们实际编写的那些具体程序，梳理常见的失败模式，并为这些场景开发有针对性的工具。经验研究——例如对分布式系统中错误处理的分析——往往比追求不可能实现的通用验证器更具实用价值。只要承认复杂度是根本性的约束，并把精力投入到我们所构建软件中那些具体、可衡量的属性上，就能在不追求完美的前提下稳步提升可靠性。
Writing correct software is fundamentally difficult because the nature of computation itself imposes unavoidable constraints. Theoretical computer science, rooted in the foundational work of Gödel, Church, and Turing, established that we cannot fully understand or predict the behavior of arbitrary programs. The halting theorem proves that no algorithm can determine if a program will eventually terminate, and its corollaries, such as Rice's theorem, demonstrate that deciding any non-trivial property of a program's behavior is similarly impossible. These results indicate that programs and the complete understanding required for perfect correctness are essentially at odds.
Computational complexity adds another layer of reality to these limitations. It is not enough for a problem to be decidable in theory if the resources required to solve it exceed reasonable bounds. Even when problems are technically solvable, the time and effort required often grow to levels that are practically insurmountable. As researchers like Juris Hartmanis and Richard Stearns observed, complexity functions as a law of nature. Results show that we cannot analyze a program's behavior faster than the program itself runs. Consequently, verification, viewed as a decision problem, is among the hardest challenges in computer science, and correctness cannot simply be broken down into modular, manageable components.
Abstractions in programming languages, such as high-level structures, functions, and concurrency, do not magically bypass these core difficulties. While these features make programs easier for humans to write, they do not simplify the underlying state space in a way that makes verification generally feasible. Even for finite state machines, where verification is theoretically possible, the problem is often PSPACE-complete. This means that programs with succinct representations are not necessarily easier to verify than their more verbose counterparts. The state explosion problem remains a significant hurdle for automated model-checkers, which must grapple with the sheer, often irregular complexity of real-world software.
Various approaches to verification, including model checking, deductive proofs, and static analysis, each operate within these rigid boundaries. Techniques like abstract interpretation or type systems attempt to make verification tractable by sacrificing precision, providing sound but incomplete results. While these tools assist in identifying specific classes of bugs, they cannot guarantee total correctness for all programs. The attempt to find a single, universal solution to software reliability is essentially modern alchemy. As Fred Brooks noted, there are no silver bullets in software engineering, and we must accept that complexity is an essential feature of the systems we build.
Ultimately, the most pragmatic path forward is to embrace an empirical, ad hoc approach similar to the physical sciences. Since we cannot verify all programs, we should study the specific programs humans actually write, document the common patterns of failure, and develop targeted tools for those scenarios. Empirical studies, such as the analysis of error-handling in distributed systems, offer far more practical value than the pursuit of impossible universal verifiers. By accepting that complexity is a fundamental constraint and focusing on specific, measurable properties of the software we create, we can make steady progress in improving reliability, even if perfection remains out of reach.
141 comments • Comments Link
- 数学正确性（mathematical correctness）和现实可用性（real-world functionality）属于不同层面的目标：在人类环境中运行的软件必须应对不可预期的变量和持续变化的需求，而这些需求往往无法用严格的形式化规则来事先定义。
- 现代操作系统和硬件缺少可靠的底层基础原语（primitives），这阻碍了形式化验证：共享状态、最高权限（root access）以及环境层面的不一致性会让潜在系统状态空间呈指数级扩张。
- 软件缺陷通常来自规格（specification）层面的错误——也就是构建了错误的东西——而不是实现（implementation）本身的瑕疵。这意味着形式化验证往往只能覆盖"总失败面"中的一小部分。
- 转向数据中心型（data-centric）的操作系统和架构，可能通过降低状态管理的复杂度来让验证更容易；相较传统以文件为中心（file-centric）的设计，这种做法更有优势。
- 形式化方法（formal methods）常常受限于必须为问题空间定义清晰的"本体"（ontology）。但当涉及人的语义、跨系统互操作以及不断变化的需求时，这几乎是不可能做到的。
- 对于封闭系统来说，证明程序正确在理论上是可行的。然而对大多数商业应用而言，形式化验证的成本高得难以接受：在这些场景里，迭代速度、"能用"（fit for use）以及对市场的响应能力才是关键的生存指标。
- AI 生成代码的出现进一步凸显了人类理解（human understanding）的"壁垒"（moat）：机器可以生成功能性代码，但通常缺少支撑它与多变且非正式的业务需求保持一致的必要背景信息。
- 商业软件往往是一个不断变化的目标。利益相关者在定义上可能存在根本分歧，使得"正确性"不再是纯数学意义上的概念，而更像一个带有主观性与政治色彩的判断。
- 轻量级的形式化方法与类型系统提供了一个更可行的折中：开发者可以把关键假设编码进去，并验证关键组件，而不必为每一行代码都付出绝对证明的开销。
- 形式化验证在航空、医疗设备和密码学等高可靠性领域仍然是至关重要的工具，但它与大多数商业软件开发中那种创造性的、以探索为导向的工作有着本质差异。
这场讨论凸显了软件工程中对数学严谨性的追求，与商业开发所依赖的混乱经验现实之间长期存在的张力。尽管形式化验证被普遍认为是安全关键系统的强力手段，但参与者强调，软件中大部分"bug"的根源在于模糊的需求和不断变动的业务目标，而不是实现中的逻辑错误。反复出现的观点是："正确性"本质上是一种软件与现实世界匹配程度的属性——它往往是不断移动的、带主观色彩的，并由人类共识来定义。因此，尽管用于形式化规格与验证的工具越来越容易获得，人们也不会把它当作灵丹妙药，而是把它视为一种需要在开发速度与不断演进的规格需求之间进行权衡的专门工具。 • Mathematical correctness and real-world functionality are distinct domains, as software operating in human environments must navigate unpredictable variables and evolving requirements that defy formal specification.
• The lack of reliable primitives in modern operating systems and hardware hinders formal verification, as shared state, root access, and environmental inconsistencies create an infinite space of potential system states.
• Software bugs often stem from specification errors—building the wrong thing—rather than implementation flaws, meaning formal verification only addresses a small fraction of the total failure surface.
• Moving toward data-centric operating systems and architectures could potentially simplify verification by reducing the complexity of state management compared to traditional file-centric designs.
• Formal methods are often constrained by the necessity of defining a clear "ontology" for the problem space, which becomes nearly impossible when human semantics, interoperability, and changing requirements are involved.
• While proving a program correct is theoretically possible for closed systems, the cost of formal verification is prohibitive for most commercial applications where iteration speed, "fit for use," and market responsiveness are the primary survival metrics.
• The emergence of AI-generated code emphasizes the "moat" of human understanding, as machines can produce functional code but often lack the context to ensure it aligns with volatile, non-formalized business requirements.
• Business software is frequently a moving target where stakeholders may fundamentally disagree on definitions, rendering the concept of "correctness" subjective and politically charged rather than purely mathematical.
• Lightweight formal methods and type systems offer a practical middle ground, allowing developers to encode assumptions and verify critical components without the overhead of absolute proof for every line of code.
• Formal verification remains a vital tool for high-reliability domains like aviation, medical devices, and cryptography, but it is fundamentally distinct from the creative, discovery-oriented work that characterizes most commercial software development.
The discussion highlights an enduring tension between the desire for mathematical rigor in software and the messy, empirical reality of commercial development. While formal verification is acknowledged as a powerful tool for safety-critical systems, participants emphasize that much of the "bugginess" in software arises from ambiguous requirements and shifting business goals rather than logical errors in the implementation. A recurring theme is that "correctness" is a property of the fit between the software and the real world, a target that is often moving, subjective, and defined by human consensus. Consequently, while tools for formal specification and verification are becoming more accessible, they are viewed less as a panacea and more as specialized instruments that must be balanced against the practical demands of development speed and evolving specifications.