&gt; Looking to the future I hope we can find a way to achieve the level of results they do, without the ridiculous effort and cost.<p>That is unlikely. For computational complexity theory reasons, writing correct software is <i>extremely</i> computationally expensive (regardless of whether or not the language is Turing complete). In fact, it is &quot;the hardest problem in computer science&quot;, in the sense that any problem with bounded complexity can be efficiently reduced to software verification. Even verifying finite-state-machines (the simplest computational model) is PSPACE-hard.<p>What we <i>can</i> do is find many ad hoc ways, each helping to some extent with some kinds of correctness properties.