Thanks for the overview. I was hoping for some examples, but most work on it is done in academia. "Iterative" theorem proving (though probably a typo for "inte

Thanks for the overview. I was hoping for some examples, but most work on it is done in academia. "Iterative" theorem proving (though probably a typo for "interactive"), is the way this could go: "agile theorem proving". That is, where you don't need to plan ahead. i can imagine a world where people are fed up with badly written software, which will force engineering to verify at least certain properties. Historically, people consistently choose features, convenience and performance over well-written software. It seems that formal methods only get a foothold where there are serious consequences for failure - often legal ones. BTW: The US/UK vs. Germany/France in computer science seems to me (from reading papers) to be pragmatism vs. theory. Reading on electromagnetism, Lord Kelvin took French scientists to task to task for their errors traceable to their algebraic and abstract methods - so this divide seems to go back a ways.