为什么编写正确的软件如此困难
Why Writing Correct Software Is Hard
很多人认为有了合适的工具，软件正确性就唾手可得，但这忽略了计算的“自然法则”。文章从大卫·希尔伯特的数学形式化计划讲起，回顾哥德尔不完备定理和图灵停机问题如何揭示了程序与完全理解之间的根本矛盾。无论是动态运行还是静态分析，验证程序正确性的成本都源于计算理论的本质限制。甚至存在仅几百行代码的微小程序，其行为在 ZFC 公理体系下都无法被数学证明是否终止。正确性并非易事，它需要付出巨大的代价。
正确性的代价——就像降低熵所需的能量代价一样——是计算“自然法则”的结果，是绝对无法避免的。
HN 评论区
126- turbobutton
我认为软件中的抽象数学正确性与现实世界的实际运行之间存在一条清晰的界限。任何处理输入并为人类提供复杂工作流的软件，都必然要应对现实中无穷无尽的不确定性。
这并非说形式化正确性没有价值，但关键在于识别何时它是有用的，何时它带来的麻烦超过了其价值……
- hinkley
我过去常说一句话，最近没怎么提了，虽然我不确定为什么，但我依然坚信：
软件本质上就是合同法，如果其中一个能解决，另一个也能。我们拥有如此多的律师，且漏洞问题层出不穷，这与我们拥有如此多的程序员和如此多的 Bug 是同一个原因。
我们无法同时界定什么是可接受的输入、可接受的输出以及可接受的中间状态。而这正是编写正确软件所必需的。
- mpweiher
我觉得你首先得搞清楚“正确”到底是什么意思。
是相对于形式化规格说明而言的正确吗？
我们怎么知道规格说明本身是“正确”的？靠定义吗？
- johnbender
据我所知，这篇文章错误地将 Rice 定理与“无法证明 Yedidiya 和 Aaronson 生成的那个小程序的某些性质”混为一谈，但这并不是 Rice 定理告诉我们的。相反，它告诉我们，无法提出一种通用方法，对所有程序都能正确判断其是否到达某个特定点。
对于给定的程序和一次性的证明，我们可以证明很多事情；或者如果我们通过假设循环终止来进行过度近似，我们也可以可靠地证明很多事情，但代价是可能会拒绝那些有时是正确的程序（例如类型系统）。
不过，这也许只是语言上的怪癖或是我个人的理解偏差。
- kodoman
我一直对形式化验证很感兴趣，但只写过一些玩具级别的证明和推导出的程序。
很高兴看到这篇关于该主题的旧讨论，它独立于