我在软件工程的Stack Exchange上看到这个问题：什么障碍阻止了形式化方法的大规模采用？这个问题被关闭为基于观点的问题，大多数回答都是“这太贵了！”或“网站不是飞机！”这在某种程度上是正确的，但并不能解释得太多。我写这篇文章是为了提供形式化方法更大历史背景，为什么它们实际上如此少用，以及我们为使其被使用所做的努力。在开始之前，我们需要定义一些术语。实际上并没有一个形式化方法的社区，更多的是几个小团体在草原上觅食。 这意味着不同的小组使用术语的方式各不相同。非常粗略地说，形式化方法(FM)有两个领域：形式规格是研究如何编写精确、明确的规格，而形式验证是研究如何证明事物的正确性。但“事物”包括代码和抽象系统。不仅我们使用不同的方式来指定这两者，我们通常也使用不同的方式来验证它们。为了更令人困惑的是，如果有人说他们进行形式规格，通常意味着他们同时指定和验证系统，而如果有人说他们进行形式验证，通常意味着他们同时指定和验证代码。为了清楚起见，我将把验证分成代码验证(CV)和设计验证(DV)，并类似地将规格分为CS和DS。这些术语并不是在更广泛的FM领域中使用的。我们将先讨论CS和CV，然后转向DS和DV。此外，我们可以进行部分验证，即仅验证规格的一个子集，或完全验证，即验证整个规格。这可能是证明“它从不崩溃或接受错误的密码”与“它从不崩溃或承认错误的密码且如果你三次输入错误的密码会锁定账户”之间的区别。大部分历史将假设我们进行的是完全验证。我们还应澄清一下我们正在形式化的软件类型。大多数人隐含地将软件分为高保障软件，例如医疗设备和飞机，以及其他所有软件。人们假设，形式化方法在前者中被广泛使用，而在后者中则没有必要。这种看法，甚至可以说，是过于乐观：大多数高保障软件中的人并不使用形式化方法。相反，我们将重点关注“常规”软件。最后，免责声明：我不是历史学家，虽然我试图尽量认真，但这里可能会有错误。此外，我专注于形式规格(DS和DV)，因此在我关于代码验证的任何说法中出错的可能性更大。如果你看到错误，请给我发邮件，我会修正它。 形式编码 获取规格 在我们证明我们的代码是正确的之前，我们必须知道什么是“正确”。这意味着必须有某种形式的规格，或者说规格，来确定代码应该做什么，一种我们可以明确表示特定输出是否符合该规格的规格。仅仅说一个列表是“已排序的”是不明确的：我们不知道我们在排序什么，使用什么标准，甚至我们对“排序”的意思是什么。相反，我们可以说“一个整数列表l在升序中排序，如果对于任何两个索引i和j，若i < j，则l[i] <= l[j]”。代码规格大致分为三个主要类别：第一种是将它们写成独立于代码的声明。我们会编写我们的排序函数，并在一个单独的文件中写下定理“这返回已排序的列表”。这是最古老的规格形式，仍然是Isabelle和ACL2所采用的方式。 第二种是将规格嵌入代码中，形成前置/后置条件、断言和不变式。我们可能会在函数上添加一个后置条件：“返回值是一个已排序的列表”。基于断言的规格最初被形式化为霍尔逻辑，并在20世纪70年代初第一次与编程语言Euclid结合使用。这种风格也称为合同设计，是工业验证中最流行的形式。 最后，我们有类型系统。根据卡里-霍华德对应关系，任何数学定理或证明都可以编码为依赖类型。我们可以定义“已排序列表”的类型，并声明我们的函数有类型签名[Int] -> Sorted [Int]。你可以查看 Let’s Prove Leftpad 上所有这些的示例。HOL4和Isabelle是“独立定理”规格的良好示例，SPARK和Dafny具有“嵌入断言”规格，Coq和Agda具有“依赖类型”规格。如果你稍微眯一下眼睛，你会发现这三种代码规格形式映射到自动正确性检查的三个主要领域：测试、合同和类型。这并不是偶然。正确性是一个光谱，形式验证是该光谱的一端。当我们降低验证的严格性（和努力）时，我们得到更简单、更狭隘的检查，无论这意味着限制探测的状态空间、使用更弱的类型，还是将验证推向运行时。任何完全规格的方法……