what's the difference between lean, f*, and dafny?

Question

They are from Microsoft and seem like they are proof assistants? Besides syntactical differences are there practical aspects that make them different from one another (say ability to do automation, expressive power, etc)? I am new to formal verification.

Edit: I am not asking for which one is better, am merely interested in a technical comparison between the different features offered by these tools. I'm looking for something like this

Answer 1

Each tool has a unique design, and is built and influenced by different people with different goals and philosophies, but the authors are all friends and have sat within a few offices of each other for many years.

Rustan Leino designed Dafny as a successor to many of the systems he built before including ESC Java, and Spec#.

Dafny is based on a Java or C# like imperative language with the ability to write Hoare logic style state invariants, this allows users of the languages to verify properties about methods, and objects that use mutable state, loops, arrays, and so on. Dafny's core theory is a custom program logic mostly designed by Rustan and a handful of collaborators. Dafny discharges the verification conditions it generates by compiling them to Boogie an intermediate verification language, which in turn compiles them into queries which are passed to an SMT solver such as Z3 or CVC4 to discharge.

Dafny's design goal is to feel very similar to imperative object oriented languages users are familiar with the added ability to verify your programs.

F* is based on a new type theory designed by Nikhil Swamy and collaborators, it began as an ML like programming language with the addition of refinement types which were discharged in the style of Dafny, but has evolved substantially in the past few years due to numerous outside additions, as well as influences from Dafny, Lean, LiquidHaskell, and so on.

F*'s also translates its verification conditions to SMT solvers like Dafny, but does not use an intermediate verification language like Boogie. F* has recently gained the ability to use tactics heavily influenced by the Lean tactic language.

F*'s main innovation over tools like Dafny and other refinement types is the use of Dijkstra Monads a way to describe the "effect" of code, giving the effect designer control over the verification conditions generated. DMs allow users to reason at different levels, for example code in the Pure effect can not use state, or throw exceptions and the user is able to ignore effectful features they don't use.

Lean's design is heavily influenced by Coq and other intensional type theories and is much more similar to them, the goal of Lean is to marry the best of automated and interactive theorem provers, by bringing techniques from the automated (SMT) world to the type theory world. It has very powerful meta-programming abilities, and has been gaining more and more automation. Lean does not require an SMT solver and reimplements many of the core procedures in a specialized way for Lean's type theory.

You can view F* and Lean as covering to a similar spaces but emphasizing different ways of getting there.

I am happy to elaborate more if this doesn't clarify.

Source: core developer of Lean, developer of F*, and sometime user and contributor to Dafny, worked at MSR for ~7 months and personally know all of the tool authors.