文章探讨了形式化方法未被广泛采用的原因，指出其成本高、适用场景有限（如非航空领域），并分析了形式化方法社区分散、术语混乱等历史背景，同时提及当前改进其可用性的努力。

好的，这是根据您的要求，对原文主要内容进行的中文重述，保留了核心细节，并删减了与主题无关的评论和脚注。

标题：为什么人们不使用形式化方法？

核心问题： 软件工程领域常讨论“形式化方法”为何未被广泛采用。常见的解释（如“成本太高”或“网站不是飞机”）过于片面。本文旨在从历史角度，更全面地分析其未被广泛使用的原因，以及当前为推广它所做的努力。

关键概念澄清： * 形式化方法并非一个统一的社区，而是由多个小团体组成。它主要分为两大领域： * 形式化规约：研究如何编写精确、无歧义的规约。 * 形式化验证：研究如何证明事物（代码或系统设计）的正确性。 * 为清晰起见，本文将验证分为代码验证和设计验证，规约也相应分为代码规约和设计规约。 * 验证可以是部分验证（只验证规约的子集）或完全验证（验证整个规约）。 * 本文主要讨论“常规”软件，而非高安全性软件（如医疗设备），因为即使在后者中，形式化方法也未被普遍使用。

第一部分：形式化编码

1. 获取规约： 在证明代码正确前，必须先明确“正确”的定义，即编写规约。代码规约主要有三种形式： * 独立定理：将规约写成独立于代码的数学定理（如Isabelle, ACL2）。 * 嵌入式断言：将规约以前置/后置条件、断言和不变量等形式嵌入代码中（如Hoare逻辑、契约式设计，代表语言有SPARK, Dafny）。 * 依赖类型：通过类型系统编码数学定理（如Coq, Agda）。

2. “什么是正确的规约？”： 这是形式化方法面临的最大挑战之一。 * 外部质疑：通常指“验证”，即规约是否满足客户需求。反驳观点认为，验证虽不能替代验证，但可以在快速迭代后使用；同时，至少可以证明代码没有崩溃或安全漏洞等基本问题。 * 更根本的问题：我们常常不知道规约应该是什么。将人类概念（如“区分公园和鸟”）形式化是巨大的挑战，需要专门的技能。

3. 证明规约： 有了规约后，需要证明代码与之匹配。 * 早期方法：Dijkstra式的“深思熟虑”证明，但容易出错，且“被证明正确”的代码仍可能崩溃。 * 定理证明器：20世纪60年代末出现，用于辅助或自动证明。但证明本身非常困难。

4. 证明的困难： * 形式化要求极高：需要将数学直觉（如归纳法）和所有假设（如加法结合律）都严格形式化。 * 技能要求高：需要同时具备数学、计算机科学、领域知识、程序/规约细节以及定理证明器本身的知识。 * 语言特性阻碍：许多编程语言的特性（如C++的INT_MAX、别名、并发）会破坏证明。语言表达能力越强，证明越难；表达能力越弱，编码越难。 * 进展：证明助手在启发式算法、定理库等方面不断进步，硬件提升也加快了搜索速度。

5. SMT革命： SMT求解器（如微软的Z3）将部分定理转化为约束满足问题，大大简化了证明过程，使许多简单证明变得简单，复杂证明变得可行。然而，即使借助SMT，验证效率依然很低（例如，微软的IronFleet项目以3.7人年完成了5000行验证代码，相当于每天4行）。

6. 为何要费心？： 正确性是一个谱系。完全验证成本高昂，而90%-99%的正确性通常可以通过更全面的测试、模糊测试、属性测试等方法以更低成本实现。对于大多数行业，完全代码验证是浪费金钱。然而，这并不意味着形式化方法整体不经济。

7. 部分代码验证： 对代码的某些属性进行部分验证（如证明不会无限循环或越界）是可行的，但受限于语言的可用性。许多语言要么为完全验证设计，要么不支持验证。常见的做法是将特定验证（如Rust的内存安全、Pony的异常安全）内置于语言核心结构中。

第二部分：设计规约

1. 设计规约的价值： 代码验证极其困难，但许多系统问题源于组件间的交互。通过抽象掉实现细节，可以更容易地分析高层设计。形式化设计有助于明确系统需求，避免因需求模糊导致的设计错误。

2. 规约语言： 用于表示设计的语言，比代码验证语言更多样化，通常针对特定问题领域（如Z用于业务需求，Promela用于消息传递）。

3. 模型检查器： 验证设计的一种更简单方法。它通过暴力搜索状态空间，检查是否存在错误状态。优点是不需要编写证明，技能门槛低，且能提供明确的反例。缺点是处理无限状态模型（无界模型）和状态空间爆炸问题（组合爆炸）。通过优化模型和增加硬件资源可以缓解。

4. 设计规约的问题： 与代码验证的技术问题不同，设计验证面临的是社会问题：人们看不到它的价值。 * 设计与代码脱节：大多数设计语言无法自动生成代码，也无法验证现有代码是否匹配设计。程序员倾向于不信任非代码或未与代码强制同步的软件工件（如文档、图表）。 * 认知偏见：程序员通常认为他们现有的方法（伪代码、TDD等）足以保证设计正确，不愿尝试新方法。

总结： * 代码验证：技术难题，但随着定理证明器和SMT求解器的进步，使用者在增加，但短期内仍将是专业领域。 * 设计验证：技术上更容易，但面临文化障碍。作者认为这种障碍有可能被克服，就像自动化测试和代码审查最终成为主流一样。

根据评论内容，总结如下：

核心观点：形式化方法未被广泛采用的主要原因包括成本高、难度大、工具不成熟、业务需求不足，以及文化阻力。

支持形式化方法的观点： - 在特定高可靠性领域（如航空航天、医疗设备、金融科技、密码学）具有重要价值。引用：评论4 "When designing software for aircraft, pacemakers, fintechs, cryptography and DeFi protocols there is a bit of value for formal methods." - 实际应用案例证明其有效性。引用：评论8 "I found 4 different Postgres bugs... one, if triggered, would corrupt your database." - 可结合AI降低使用门槛。引用：评论19 "AI ought to be able to adopt the formal methods humans have used to work around the inability to verify something just by looking at it hard."

反对或质疑形式化方法的观点： - 大多数软件业务需求不要求完美。引用：评论11 "Most programs don't need to be rigorously perfect." - 学习曲线陡峭，工具不友好。引用：评论10 "I don't understand any of the material I've read describing them." - 规范本身可能出错，无法保证绝对正确。引用：评论12 "The formal spec has a bug... no amount of model checking or SMT solvers can guard you against a bug in that 'code'." - 代码变化太快，难以形式化。引用：评论20 "All our code changes too much, we wouldn't be able to formalize it before it needed to change."

平衡性观点： - 形式化方法应视为测试的补充而非替代。引用：评论12 "It's another tool next to testing, not instead of it." - 部分验证（如类型检查）已广泛使用。引用：评论6 "We do. It's called a type checker." - 行业文化差异导致采用率不同。引用：评论4 "95% of the time, the stakes are low... 5% of the time, the engineers don't understand the value of formal methods."