3 ms·

But are those backends complete? I.e. do they support all of Dafny? Last I programmed in Dafny I don't think any alternative back end did. Also Dafny has prett

But are those backends complete? I.e. do they support all of Dafny? Last I programmed in Dafny I don't think any alternative back end did. Also Dafny has pretty poor IDE support. I don't think it has Visual Studio support and the plugin for Visual Studio Code is not written by MS (and is pretty bare bones). MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support.

MaxBarraclough 6y ago
> Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support. Correct, it's been used in numerous life-or-death systems. Perhaps most famously, the software of the Boeing 777 is almost entirely SPARK based. [0][1] Dafny has not, it seems to be more of a research project. > MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Right. It would be interesting if Microsoft decided to compete in the critical-systems space, but I doubt they will. With SPARK Ada, all the real work seems to happen at AdaCore. [2] There are various different high-assurance Ada compilers available though. [0] https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf [1] https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014-intro.pdf https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014... [2] https://www.adacore.com/ https://www.adacore.com/