50年后：反对形式化验证的理由
在一篇对 1979 年著名批评的回顾中，软件形式化验证再次成为讨论焦点。许多人认为，虽然对混乱的现实系统做端到端证明仍不现实，但对关键组件（如分布式数据存储、编译器、策略引擎）进行定向验证既可行又有价值。评论者指出，严谨地规格化行为往往比写代码更难，模型—代码鸿沟与不断变化的需求限制了证明的适用范围，而且大多数真实故障其实源于有缺陷或不一致的规格，而不是实现 bug。大家对强类型系统、更好的工具以及 AI 辅助能让形式化方法更易用抱有谨慎乐观，但也担心证明会固化糟糕设计，而经济激励仍然更偏向“够用就好”的软件，而非数学上保证正确的软件。
形式化验证的范围与实用性
- 许多人认为，对于社交网络、GUI 这类混乱且不断演化的产品，做全系统验证不可行，但也同意验证特定子系统和性质是有价值的。
- GUI 被认为尤其难以规格化；有人提到基于约束的 GUI 方法更接近规格，主要用于防止明显的界面错误。
- 几条评论强调，并不需要“全有或全无”：验证权限、API 幂等性、分布式一致性以及数据不丢失性质，已经非常有用。
形式化验证 vs 测试
- 验证被描述为对所有执行都保证性质，而测试只是抽样执行。
- 性质测试和变异测试被讨论为中间技术；fuzzing 和随机测试则受益于清晰的规格。
- 有人认为我们应把形式化方法看作“加强版测试”，而不是替代品。
规格：收益、难度与正确性
- 对“规格是否比代码更容易理解”存在分歧：有人觉得形式化规格更简洁、更接近意图；也有人觉得它们比实现更难。
- 文中引用了历史例子（浮点运算、压缩、文件系统、数据库、网络），这些例子中规格很简单，但实现很复杂。
- 关于“排序”的一段长讨论说明，看似平凡的规格也容易出微妙错误，进一步表明写对规格本身就很难。
- 有人提出疑问：为什么要假设规格比程序更正确？回应是：检查通常比构造更容易；规格可以更简单；但规格错误确实存在，必须像 bug 一样对待。
经济、激励与监管
- 类硬件的经济学逻辑（一个 bug 可能造成数百万损失）足以证明重度验证的合理性；而软件通常依赖廉价补丁来应对。
- 有人认为，稳健的软件其实已经存在于愿意付费的领域（银行、航空）；但也有人指出，面向普通消费者的软件仍然充满 bug。
- 有人担心监管式的“验证印章”会变成官僚化的形式主义，而不带来真正的质量提升。
AI、工具与模型—代码鸿沟
- 过去的限制包括记号体系不佳和算力不足；如今的 SAT/SMT 求解器、证明辅助器和 LLM 减轻了部分负担。
- AI 目前在专家手中最有效；有人希望未来代理能为具有简单不变量的深层模块生成规格和证明。
- 模型—代码鸿沟（例如 TLA+ 规格与 Rust 代码之间的差距）被视为核心问题；建议的缓解方式包括：
- 能生成可执行代码的证明辅助器。
- 像 SPARK/Ada、更丰富的类型系统、经过验证的策略引擎这类让规格与代码紧密集成的语言和生态。
- 也有人担心，证明和细粒度测试会冻结糟糕的抽象，并妨碍重构。
需求 vs 实现
- 几位参与者认为，在许多真实项目中，主要失败来自不一致或不可能实现的需求，而不是代码错误。
- 他们建议，更需要的是帮助将需求形式化并验证其是否符合技术与业务约束的工具，而不仅仅是验证实现。