3 ms·

Microsoft Research is also behind Dafny and Lean and a whole bunch of more specialized tools: https://rise4fun.com/ https://rise4fun.com/ They are very wisely

Microsoft Research is also behind Dafny and Lean and a whole bunch of more specialized tools: https://rise4fun.com/ https://rise4fun.com/ They are very wisely not claiming that any of these is the verified programming language to rule them all. There is still a lot to learn.

mcguire 9y ago
Dafny is pretty damn cool, though. And it handles the major problem of other verification environments (SPARK, Frama-C) (by using garbage collection).
sevensor 9y ago
Much of this uses Z3 under the hood, and Z3 is made of pure wizardry.