Hacker News Reader

https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe

View on HN

Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts).

It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT.

But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1].

[1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf

Agree it’s not a toy. AWS implemented a large chunk of IAM in Dafny. Though IIRC they have their own non-public compiler to Java

F* also uses SAT/SMT, specifically Z3.

Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.

Reply on news.ycombinator.com