It does look cool but I’ve also been hearing about Dafny since being blown away by Microsoft’s Ironclad project published in late 2014[0]. At the time I thought all the software we write would be formally verified within a decade. Also at that time I was mulling over to myself whether I wanted to get into formal methods or AI. Now one of those is a clear winner, not the one I chose!
I know that formal methods adoption is slow generally (I’m in the TLA+ community!) but have there been any large software projects using it in the interim? (edit: per the video there’s an ethereum VM implementation in Dafny now)
I also wonder how Dafny compares to SPARK Ada 2014, or newer languages focusing on dependent types.
Videos are the worst format for me, so I didn’t watch it. I saw they mention Daphne though, which looks pretty cool:
https://dafny.org/
It does look cool but I’ve also been hearing about Dafny since being blown away by Microsoft’s Ironclad project published in late 2014[0]. At the time I thought all the software we write would be formally verified within a decade. Also at that time I was mulling over to myself whether I wanted to get into formal methods or AI. Now one of those is a clear winner, not the one I chose!
I know that formal methods adoption is slow generally (I’m in the TLA+ community!) but have there been any large software projects using it in the interim? (edit: per the video there’s an ethereum VM implementation in Dafny now)
I also wonder how Dafny compares to SPARK Ada 2014, or newer languages focusing on dependent types.
[0] https://www.microsoft.com/en-us/research/publication/ironclad-apps-end-to-end-security-via-automated-full-system-verification/