3 ms·
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).
by nextos 2y ago
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 https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
- gsbcbdjfncnjd 2y agoF* also uses SAT/SMT, specifically Z3.
- nextos 2y agoSure, 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.
- fovc 2y agoAgree 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