为什么没人使用形式化方法？
Why Don't People Use Formal Methods?
我在 Software Engineering Stack Exchange 上看到关于形式化方法推广障碍的讨论，发现多数回答过于简化。形式化方法并非只适用于医疗或航空等高保障软件，普通软件同样需要。文章梳理了形式化规范与验证的历史，区分了代码验证与设计验证，并探讨了如何编写正确的规范。验证代码正确性只是第一步，真正的挑战在于如何将人类需求转化为数学表达。尽管存在验证成本高、规范难定义等问题，但形式化方法在防止系统崩溃和安全漏洞方面价值巨大。
验证代码正确性并不能验证代码本身是否满足用户需求。
HN 评论区
115- malisper
我最近遇到了一个形式化方法极其有用的场景。我正在用 Rust 重写 Postgres，目前正专注于正确性问题。最大的挑战在于需要覆盖的表面积太大了。Postgres 有超过 3000 个面向用户的功能，从正则表达式匹配、JSON 迭代到计算 Gamma 函数，应有尽有。其中大约一半是简单的纯函数。
在这 3000 个函数中，我已经能够形式化验证其中超过 1000 个函数的 Rust 行为与 Postgres C 语言行为完全一致。在这个过程中，我发现了 4 个 Postgres 的 Bug。所有这些 Bug 在普通使用场景下都不会被触发，但其中一个如果被触发，会导致数据库损坏。
我认为形式化方法之所以在这里行之有效，是因为我在测试大量小型到中型的自包含代码片段。对于每一个片段，规范都很简单：postgres_fn(args) 是否等于 pgrust_fn(args)。我一直在使用 Kani[0]，它同时支持 Rust 和 C 代码，因此证明是基于实际代码进行的，而不是基于将代码翻译成另一种语言。
如果你想看看这些验证长什么样，可以来这里查看[1]
- teiferer
对我来说，"这返回排序后的列表"这句话道出了问题的核心。
你可能非常清楚自己想要什么，也可能有一种相当快速且廉价的方法来根据形式化规范验证你的代码。但是，形式化规范必须来自某个地方，而对于任何非琐碎的程序，其复杂度将与实现它的代码处于同一数量级。于是我们又回到了编写“代码”（形式化规范本质上就是代码）的阶段，而这部分代码需要对照我们真正想要的内容进行检查。而这部分“代码”需要……测试吗？深思熟虑吗？还是形式化验证本身？
不相信我说这很难？回到“这返回排序后的列表”这个例子。形式化验证的承诺是：无论我提交给验证器的实现是什么，只要它通过了检查，我就很满意（假设我还能编码运行时间和资源使用情况等）。现在想象一个总是返回空列表的程序。它平凡地满足了“这返回排序后的列表”这一条件，但这完全不是我们想要的。形式化规范本身有 Bug。在大型项目中，这类问题可能很微妙，无论多少模型检查或 SMT 求解器都无法保护你免受该“代码”中 Bug 的影响。
别误会，它确实可能极其有用。但它并不是某些支持者所宣称的那种万能灵药。它是与测试并列的另一种工具，而不是用来替代测试的。（那种“测试只能证明 Bug 的存在，而不能证明其不存在，所以我们应该用形式化验证来替代测试”的说法，轻则只是 misguided，重则……”
- ndriscoll
我们确实在用。它叫类型检查器（type checker）。每一个“形式化验证”的系统都只能做到部分验证。例如，你可能证明了你的排序过程确实能排序，但你证明过它的复杂度吗？是基于整数比较的成本模型，还是基于页面获取（page fetches）的成本模型？或者是两者都有？多层缓存的页面获取成本呢？你的验证程度完全取决于你决定如何对问题进行建模。不同的类型检查器具有不同的建模特性。
这是一个更有用的视角：问题不在于“我们用不用形式化方法”，而在于“我如何更精确地对我的领域进行建模？”有趣的是，如果你能很好地对领域进行建模，代码往往会变得显而易见，甚至像是自己写出来的。
- SCdF
在大多数需要软件的行业里，让人们愿意花足够的时间去关注非形式化方法（informal methods）都已经够难了，更不用说形式化方法了。我根本不认为大多数行业拥有足够的缓冲空间和工程文化尊重，让这种模式得以发展。
- asxndu
我认为这是软件工程文化的锅。
在开发外卖应用或社交网络时，使用形式化方法似乎是在浪费时间。
但在设计飞机软件、起搏器、金融科技、密码学以及 DeFi 协议时，形式化方法确实有一定价值。
问题在于，往往那些拥有外卖应用或社交网络文化的人被雇佣来构建 DeFi 协议。
这也解释了为什么近期有这么多资金从 DeFi 协议中被盗。
所以，为什么人们不使用形式化方法？
- 95% 的情况下，风险很低。
- 5% 的情况下，工程师们不理解形式化方法的价值。
Leslie Lamport 曾开玩笑说，如果软件开发者是建筑师，他们会先建好摩天大楼，然后再画蓝图。