> Having been down this road [1], a big problem is that the people doing this tend to be too much into the theory and not enough into wanting programs not to cr

> Having been down this road [1], a big problem is that the people doing this tend to be too much into the theory and not enough into wanting programs not to crash. This problem is already solved. Instead of crashing - do something else! Like make a so-called “educated guess” of what the program should actually do. Or throw you into a debugger. Or, heck, do as JavaScript does: if you can't figure out what the right thing to do is, do something wrong instead! The actual unsolved problem is how to write correct programs. I'm skeptical that mechanizing formal verification is the solution.