是的。答案是肯定的。打脸了，Betteridge。
本周早些时候，我在 TLA+ 会议 2024 做了主题演讲。我在演讲中的信息是我长期以来一直认为的真理：正规方法是良好的软件工程实践的重要组成部分。如果你是一名软件工程师，尤其是从事大规模系统、分布式系统或关键低级系统工作的工程师，而没有将正规方法作为你的方法的一部分，你可能会浪费时间和金钱。
因为从根本上说，工程是优化时间和金钱的练习。
“如果工程学不再被普遍认为甚至被定义为建造的艺术，那就好了。从某种重要意义上说，它更像是不建造的艺术；或者粗略但不无道理地定义，它是用一美元做好任何笨手笨脚的人可以用两美元做的事情的艺术。” — Arthur Wellington
乍一看，这可能显得反直觉。正规方法并不便宜，也不是特别容易，并且不适合每种软件工程方法。合理地认为，正式方法会增加成本，特别是非重复性工程成本。但我的经验是，这并不是真的，有两个原因。首先是返工。软件工程在工程领域中有点独特，因为设计和建造往往同时发生，而且很多建造可以在设计没有深入之前就开始。这在电气工程（设计 PCB 或布线不能在设计完成之前进行）、土木工程（在不知道要建什么之前开始土方工程是可能的，但可靠的浪费钱的方法）或机械工程中并不是真实的，等等。这是软件的一个巨大优势——其可变性是其征服世界的原因之一——但也可以显著增加设计迭代的成本，将设计迭代变成实施迭代。第二是变更成本。一旦 API 或系统有了客户，改变它会变得更加昂贵和困难。这与 Hyrum 的定律根本相关：
有足够多的 API 用户后，无论你在合同中承诺什么：系统的所有可观察行为都会被某人依赖。
隔离具有 API 的系统行为是个好主意。事实上，我认为这是所有软件工程中最重要的想法之一。Hyrum 的定律提醒我们这种方法的局限性：用户最终会依赖于 API 的每一个可想象的实现细节。这并不意味着改变是不可能的。在我的职业生涯中，我参与了许多项目，完全重新实现了 API 背后的系统。这仅仅意味着变更是昂贵的，并且诸如 API 之类的抽象并不能有效地改变这种现实。
通过节省返工成本，并在早期解决接口变更，正规设计工作可以显著提高软件构建过程的速度和效率。
什么样的系统？
这似乎不适用于所有类型的软件。由快速发展的或难以正式化的用户需求驱动的软件，从用户界面和网站到定价逻辑实现，可能需要大量持续的返工，以至于前期设计的价值被稀释（或其成本显著增加）。这是敏捷背后的基本思想：通过并行运行实现和需求收集，可以减少实际上市时间。更重要的是，在需求收集是一个持续过程时，它允许实现即使在需求不断演变时也能完成。在许多情况下，这种并行开发方法是最优的，甚至是取得任何进展所必需的。
另一方面，大规模、分布式和低级系统背后的许多软件都有很好的需求理解。或者至少，一个足够大的已知静态需求子集，使前期正式设计显著减少了实现阶段（以及之后，当系统投入生产时）的返工和错误密度。
关于前期设计与敏捷之间的争论大多来自于软件光谱两端的人们互相交谈时互不理解。我们不应该对需求收集模型非常不同的软件有不同的最佳工程方法感到惊讶。看起来需求过程越接近物理定律，在工程过程中设计和正规设计就越有价值。需求越接近用户意见，它们就越不有价值。
这并不意味着明确写下用户需求没有价值，也不意味着探索正式指定它们的方法没有价值。正式或非正式地写下需求是极其有价值的。不写下来可能会浪费很多时间，并导致很多摩擦，因为人们最终会朝不同方向拉动。然而，这确实意味着正式指定所有形式的人类需求通常很难（也许不经济）。例如，我不知道如何指定用户界面美学要求、文档可读性甚至 API 命名一致性。
哪些工具？
正规方法和自动推理是广泛的领域，有大量工具。在我的职业生涯中，在大型云系统领域中，我发现以下工具有用（但我确信如果我知道它们，我会发现更多有用的工具）。
- 像 P、TLA+ 和 Alloy 这样的规格语言，以及它们相关的模型检查器。
- 像 turmoil 这样的确定性模拟工具，它们与模糊测试一起允许通过测试有原则地搜索状态空间。
- 像 Dafny 这样的验证感知编程语言和像 Kani 这样的代码验证器。我不是这些工具的深度专家，用得少一些。
- 数值模拟技术。我倾向于自己构建（如前所述），但市场上有许多框架和工具。
- 白板上的准正式方法。这些方法包括在白板上或设计文档中绘制决策表、真值表、显式状态机等。
我也喜欢《Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3》中的方法调查。这是一个很好的起点。
但正如本文所述，我们不应过于执着于认为验证实现是唯一有价值的最终目标。这确实是一个有价值的目标，但我发现使用像 TLA+ 和 P 这样的工具在构建之前更快、更具体地思考设计非常有价值。
更快的软件，更快
回到 2015 年，当我们为 CACM 编写《How Amazon Web Services Uses Formal Methods》时，我非常关注正确性。关注验证设计的安全性和活性属性，以及更快地获得正确设计。在与一个使用 TLA+ 内部锁管理系统团队交谈时，我发现了一些我更喜欢的东西。这些话，来自表 1：
验证了一个激进的优化
这令人耳目一新。不仅像 TLA+ 这样的工具帮助我们更快地构建系统，它们还帮助我们构建更快的系统。它们允许我们快速探索可能的优化，找到真正重要的约束，并检查我们提出的优化是否正确。在许多情况下，它们消除了许多系统可能陷入正确性与性能之间艰难权衡的问题。
结论
在设计阶段使用工具帮助我们思考系统设计可以显著提高软件开发速度、降低风险，并允许我们从一开始就开发出更优化的系统。对于那些从事大规模和复杂系统工作的人来说，它们只是良好工程实践的一部分。