dafny - 精益、f* 和 dafny 有什么区别？

Question

他们来自微软，似乎他们是证明助理？除了语法上的差异之外，还有哪些实际方面使它们彼此不同（比如自动化能力、表达能力等）？我是形式验证的新手。

编辑：我不是在问哪个更好，我只是对这些工具提供的不同功能之间的技术比较感兴趣。我正在寻找这样的东西

Answer 1

每个工具都有独特的设计，并且是由具有不同目标和理念的不同人构建和影响的，但作者都是朋友，并且多年来一直坐在彼此的几个办公室里。

Rustan Leino 将 Dafny 设计为他之前构建的许多系统的继承者，包括 ESC Java 和 Spec#。

Dafny 基于类似 Java 或 C# 的命令式语言，能够编写 Hoare 逻辑风格的状态不变量，这允许语言的用户验证有关使用可变状态、循环、数组等的方法和对象的属性。Dafny 的核心理论是自定义程序逻辑，主要由 Rustan 和少数合作者设计。Dafny 通过将其生成的验证条件编译为中间验证语言 Boogie 来释放验证条件，Boogie 又将它们编译为查询，这些查询传递给 Z3 或 CVC4 等 SMT 求解器以释放。

Dafny 的设计目标是感觉与用户熟悉的命令式面向对象语言非常相似，这些语言增加了验证程序的能力。

F* 是基于 Nikhil Swamy 和合作者设计的一种新类型理论，它最初是一种类似于 ML 的编程语言，增加了以 Dafny 风格推出的细化类型，但在过去几年中已经有了很大的发展，原因是许多外部添加，以及来自 Dafny、Lean、LiquidHaskell 等的影响。

F*'s 还将其验证条件转换为 Dafny 等 SMT 求解器，但不使用 Boogie 等中间验证语言。F* 最近获得了使用深受精益策略语言影响的策略的能力。

F* 对 Dafny 和其他细化类型等工具的主要创新是使用 Dijkstra Monads 来描述代码的“效果”，让效果设计师可以控制生成的验证条件。DM 允许用户在不同级别进行推理，例如Pure效果中的代码不能使用状态，或者抛出异常并且用户能够忽略他们不使用的有效功能。

Lean 的设计深受 Coq 和其他内涵类型理论的影响，并且与它们更相似，Lean 的目标是通过将自动化 (SMT) 世界中的技术引入类型理论来结合最好的自动化和交互式定理证明器世界。它具有非常强大的元编程能力，并且越来越自动化。精益不需要 SMT 求解器，并以精益类型理论的专门方式重新实现了许多核心程序。

您可以将 F* 和 Lean 视为对相似空间的覆盖，但强调到达那里的不同方式。

如果这没有澄清，我很乐意详细说明。

资料来源：Lean 的核心开发人员，F* 的开发人员，有时也是 Dafny 的用户和贡献者，在 MSR 工作了大约 7 个月，并且个人认识所有工具的作者。