> 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 li

> 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/