4 ms·
Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ http
by digitalice 4y ago
Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- tgv 4y agoLooks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.
- hath995 4y agoIt is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.
- tgv 4y agoThanks. Pretty cool.