4 ms·
https://dafny.org/ 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 beli
by akkad33 2y ago
https://dafny.org/ 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
- nextos 2y agoHaving 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
- deleted 2y ago[deleted]