Marc Brooker 这篇文章讨论了形式化方法在软件工程实践中的重要性，特别是在构建大型系统、分布式系统或关键的低级系统时，在这些情况下不使用形式化方法很可能会浪费时间和金钱。
形式化方法并不便宜，也不是特别容易，并且并不适合每种软件工程方法。
- 人们有理由相信形式化方法会增加成本，尤其是非经常性工程成本。
我的经验是，这并非事实，原因有二：
- 首先是返工：软件工程在工程领域有些独特，因为设计和施工往往同时进行，许多施工可以在没有进行太多设计的情况下开始。这是软件的一大优势 - 它的可变性是它征服世界的原因之一 - 但也可以通过将设计迭代转变为实施迭代来显著增加设计迭代的成本。
- 是变更成本：一旦 API 或系统有了客户，更改它的成本和难度就会增加很多倍。
使用 API 隔离系统行为是一个绝妙的想法。事实上，我认为这是整个软件工程中最重要的想法之一。
- 如果 API 有足够数量的用户，那么你在API合约中倡导的什么承诺并不重要：系统的所有可观察到的行为都将依赖于某人（上下文、具体情况）。
海伦定律提醒我们这种方法的局限性：用户最终将依赖于 API 的每一个可以想象的实现细节。这并不意味着改变是不可能的。
在我的职业生涯中，我参与过许多完全重新实现 API 背后系统的项目。这仅仅意味着改变是昂贵的，而像 API 这样的抽象并不能有效地改变这一现实。
通过节省返工成本并尽早完成接口更改，正式的设计工作可以显著提高软件构建过程的速度和效率。
形式化方法有助于更快地构建系统，并通过快速探索优化和约束条件来创建更快的系统。
哪些工具？
形式化方法和自动推理是广阔的领域，拥有大量的工具。在我的职业生涯中，在我的大型云系统领域，我发现以下工具很有用（但我相信有些工具如果我了解的话会很有用）。
- P、TLA+和Alloy等规范语言及其相关的模型检查器。
- 确定性模拟工具（如turmoil）允许通过模糊测试以及通过测试搜索状态空间的原则性方法。
- 像Dafny这样的验证感知编程语言和像Kani这样的代码验证器。我对这些工具并不是很了解，而且使用它们的次数比其他工具少很多。
- 数值模拟技术。我倾向于构建自己的技术（正如我之前所写），但目前已经有很多框架和工具了。
- 白板形式化方法。这些方法包括：在白板上或设计文档中绘制决策表、真值表、显式状态机等。
但是，就这篇文章而言，我们不想太过纠结于“验证实现是唯一值得的最终目标（实践是检验真理的唯一标准）”这一想法。这确实是一个值得的目标，但我发现使用 TLA+ 和 P 等工具在构建之前更快、更具体地思考设计有很大的价值。
Brooker 文章的要点：
- 形式化方法有助于更快地构建系统，并通过快速探索优化和约束条件来创建更快的系统。
- TLA+ 和 P 等工具对于在实施前更具体地思考设计很有价值，有可能减少返工并提高效率。
- 形式化设计工作可以减少返工成本，提前解决界面变化问题，从而大大提高软件构建过程的速度和效率。
- 形式化方法的价值因软件类型而异。需求明确的系统或更接近 "物理定律 "的系统更能从形式化设计方法中获益。
- 虽然形式化方法最初可能看起来成本很高，但一旦 API 或系统有了客户，它们可以最大限度地减少返工和变更费用，从而降低总体成本。
- 形式化方法尤其适用于将系统行为与应用程序接口隔离开来，鉴于海勒姆定律（系统的所有可观察行为都会被某些人依赖），这一点至关重要。
结论
在设计阶段使用工具来帮助我们思考系统的设计可以显著提高软件开发的速度，降低风险，并让我们从一开始就开发出更优化的系统。对于我们这些从事大型复杂系统工作的人来说，它们只是良好工程实践的一部分。