50 年后反对形式验证的案例

反对形式验证的案例，50 年后工程师们对软件验证感到兴奋！这可能会让人感到惊讶，因为长期以来人们认为验证只在非常特殊的情况下有用（最好的情况是不切实际的、无用的或完全浪费时间）。然而，围绕它的炒作显然就在这里：谷歌趋势显示，过去两年中形式验证/形式方法的搜索量大幅上升，每个人都在学习精益，新的规范语言定期出现，并且有人在努力端到端地验证主要应用程序（例如，Signal Shot 项目）。这种兴奋的主要驱动力是人工智能编码。首先，人工智能代理在我们对他们编写的程序的理解中留下了漏洞，从而需要其他方法来保证正确性。其次，它们使验证本身更快、更容易融入到现实世界的软件开发中。第三，也许对商业来说最重要的是，如果编写程序变得超快，那么未来的所有收益都将集中在软件正确性保证领域。 Antithesis 的威尔·威尔逊 (Will Wilson) 在题为“我们赢了，现在怎么办？”的演讲中宣布了这一传统利基领域的胜利。 （这次演讲是 Bug Bash 2026 的开场白，非常精彩，考虑到主流的采用，它为验证社区的未来提供了一些好主意。）在这种胜利的背景下，回到反对形式验证、社会过程以及定理和程序证明的经典论文之一是很有趣的。其作者在 1979 年写道：“我们相信（……）程序验证注定会失败。我们看不出它将如何影响任何人对程序的信心。”我将仔细研究论文中的论点，并研究最近的哪些发展（如果有）使它们无效。这是一个有趣的练习，而不是一个完全严肃的练习：本文实际上并没有声称所有形式化方法的努力都注定会失败（而只是进行了全面验证）。此外，目前还不清楚验证是否会成为软件工程的常规部分（我们看到的只是早期的兴趣迹象）。尽管如此，到 2026 年重新审视 50 年前被视为根本性的障碍有望是有用且有趣的。论点 1：数学证明是关于社会过程的 在这个论点中，论文作者反对这样的观点：编程应该变得更像数学，因为每个程序都对应一个需要证明的定理。他们说：等等，即使在数学中，定理证明也不是过程的终点。相反，证明是第一步，也是一种沟通手段。当其他数学家将证明内化，并且该主张与数学或物理现实的其他分支相联系时，真正重要的部分就会发生。整个过程有助于提高主张的可信度。这里没有什么可反对的：程序的证明不需要与数学完全对应。 （这个论点是反对特定的动机，而不是反对软件验证的基本原理。） 论点 2：规范的问题 论点的第一部分是这样的：存在一些非正式的现实世界需求（所涉及的人员对需求是什么有共同的直观理解）。这种直观的、非正式的需求需要转化为正式的规范，这本身就是一个非正式的过程。在这个未经证实的过程中，很多东西可能会丢失或被误解。这是一个公平的观点。与之相反的是，规范比实现更接近非正式需求（因此更容易发现错误）。此外，现代规范语言（例如 Quint ）可以交互式地检查规范及其所有边缘情况，以确保它确实符合我们的直觉。论证的第二部分指出，规范只有独立于实现才有价值。考虑到软件开发的迭代性质，这几乎是不可能的。一旦失去独立性，我们实际上只是在调整规范和实现（并且可能会引入类似的错误）。即使在过去，我也不认为这是一个有力的论据，尤其是在循环中的编码代理的情况下。每当获得额外的理解时，这对于整个开发过程都是有好处的。人类作为最终的仲裁者，决定以何种方式改变规范，重新检查最初的假设。可以允许编码代理生成和更改代码，并生成证明。然而，如果需要修改规范，那么只有人类才能作为正确含义的最终仲裁者来做到这一点——这让我们回到了论点 2 的第一部分。 论点 3：全自动验证是遥不可及的。 在争论了为什么验证作为一种通信手段是不好的之后，