1. 9

See also https://whileydave.com/publications/pea22_gpce/

    1. 1

      Videos are the worst format for me, so I didn’t watch it. I saw they mention Daphne though, which looks pretty cool:


      1. 2

        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/