&gt; My original objection was to the claim that a non-trivial program could be demonstrated to be &quot;provably correct.&quot; This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel&#x27;s incompleteness theorems, both of which demonstrate that this is not possible.<p>You don&#x27;t need to solve the Halting problem (or find a way around Rice&#x27;s theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a <i>decision procedure</i> for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist.<p>To give an analogy, consider these two apparently contradictory facts:<p>(0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two <i>arbitrary</i> reals, loops forever if they are equal, but halts if they aren&#x27;t. You can&#x27;t do better than this.<p>(1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?]<p>The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 <i>aren&#x27;t arbitrary</i>, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure.<p>The way around the Halting problem is very similar: <i>Don&#x27;t write arbitrary programs.</i> Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former.<p>This much math you need to know if you want to lecture others on the Internet. :-p