他们来自微软，看起来像是证明助手？除了语法上的差异之外，还有哪些实际方面使它们彼此不同（比如自动化能力、表达能力等）？我是形式验证的新手。
编辑：我不是问哪个更好，我只是对这些工具提供的不同功能之间的技术比较感兴趣。我正在寻找类似this
【问题讨论】：
每个工具都有独特的设计，并且受到具有不同目标和理念的不同人的影响和影响，但作者都是朋友，并且多年来一直坐在几个办公室里。
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 效果中的代码不能使用状态，或者抛出异常，用户可以忽略他们不使用的有效功能。
精益的设计深受 Coq 和其他内涵类型理论的影响，并且与它们更相似，精益的目标是通过将自动化 (SMT) 世界的技术引入到类型论世界。它具有非常强大的元编程能力，并且越来越自动化。精益不需要 SMT 求解器，并以针对精益类型理论的专门方式重新实现了许多核心程序。
您可以将 F* 和 Lean 视为覆盖相似的空间，但强调不同的到达方式。
如果没有澄清，我很乐意详细说明。
资料来源：Lean 的核心开发人员、F* 的开发人员，以及 Dafny 的用户和贡献者，在 MSR 工作了大约 7 个月，并且个人认识所有工具作者。
【讨论】：