为什么编写正确的软件很困难

……以及为什么数学（单独）无法帮助我们，我很高兴再次在 Curry On 上发表演讲。去年，在我们与 Quasar 合作之后，我谈到了 Continuations 与 monads 。今年，我做了一个关于软件验证中的计算复杂性结果的演讲，这是我在正式指定和验证我们即将推出的 Galaxy 改进版本时开始感兴趣的主题。视频 接下来是演讲的扩展版本（嵌入在上面），其中包含一些我没有时间介绍的额外证明和结果，并附有脚注，供那些希望进一步研究该主题的人使用。阅读时间：约 45 分钟。在本文中，我们试图理解程序与正确性之间的关系，特别是为什么编写正确的程序很困难。我们将回顾可计算性理论和复杂性理论的结果，并发现程序和完整的理解（这是正确性所必需的）从根本上是不一致的。本文的主要贡献是将与生成正确软件的基本困难相关的一些结果（以及一些参考文献）聚集在一处。我的动机是我在网上找到的各种声明（例如这个，尽管它远不是唯一的）声称使用正确的工具可以轻松实现软件的正确性。虽然某些工具可能（并且确实）确实有助于确保程序正确，但正确性需要付出巨大的代价。正确性的成本——就像减少熵的能量成本——是计算“自然法则”的结果，这是不可能避免的。第一章：基础 理论计算机科学的故事大约始于一百年前。随着数理逻辑的日益成功，数学家大卫·希尔伯特制定了一个将所有数学形式化的计划。他想证明形式主义的一致性和完整性，并找到一种决策程序，一种确定每个形式陈述的真实性的算法： 一致性：证明形式主义中不能得到矛盾。完备性：所有真实的数学陈述都可以在形式主义中得到证明。可判定性：决定任何陈述是否为定理（Entscheidungsproblem）的算法希尔伯特相信任何可以形式推理的东西也可以被完全理解，我的意思是它的所有属性都被证明。 19世纪关于知识有限的观点用格言“ignoramus et ignorabimus”来表达，意思是“我们不知道，我们也不会知道”。 1930 年退休时，希尔伯特在柯尼斯堡向德国科学家和医生协会发表了题为“Naturerkennen und Logik”（逻辑和对自然的理解）的演讲，对这一观点提出了挑战。他说：对于数学家来说，没有无知者，在我看来，对于自然科学来说也根本没有。 ……在我看来，[没有人]成功找到无法解决的问题的真正原因是，不存在无法解决的问题。与愚蠢的无知者相反，我们的信条主张：我们必须知道，我们应该知道！这些话——Wir müssen wissen。 Wir werden wissen – 刻在他的墓碑上。当时希尔伯特并不知道，当库尔特·哥德尔试探性地宣布他的第一个不完整结果时，他的程序已在一天前被废除。哥德尔的不完备性定理推翻了希尔伯特纲领的前两个支柱（有人说还有第三个支柱，只是他没有意识到这一点），1936 年，丘奇和图灵通过今天所谓的停止定理的证明，打破了第三个支柱，即决策问题。停止定理——CS 的第一个定理——在 1936 年阿隆佐·丘奇和艾伦·图灵的论文中得到了证明。该定理对于计算的本质来说是如此基础，以至于它与两种计算公式一起出现并非偶然。它指出不存在一种算法可以决定任何给定程序是否终止。该证明（此处以缩写形式给出）基于对角化或自引用的思想，这与哥德尔在其不完备性证明中使用的思想相同。假设这样的程序 H 存在： H(M, x) := IF M 在 x 上暂停 THEN TRUE ELSE FALSE 我们可以轻松构造 $G$: G(y) := IF H(y, y) = FALSE THEN TRUE ELSE 永远循环 如果我们将 $G$ 传递给它自己 ($G(G)$)，我们就会得到 $G$ 所做的事情和 $H$ 所说的 $G$ 所做的事情之间的矛盾。有趣的是，停止定理立即产生了哥德尔第一个不完备性定理的一个版本。证明很简单：假设对于每个真实的陈述，在某种逻辑理论（基本上是一组公理）中都有一个逻辑证明。那么，给定一个程序，从这些公理出发，我们可以通过逻辑演绎将所有定理一一列举出来。因为所有陈述的数量，更不用说所有定理，都是可数的，并且因为每个陈述要么有证明，要么它的否定有，所以我们最终会找到其中一个或另一个的证明。因此，给定一个程序，我们可以开始