That is a very common but incorrect misinterpretation of the halting problem.<p>The halting problem says that there exist programs that cannot be proven correct; it says that for any property you want to prove computationally, no program can give you an answer for every last program. It doesn&#x27;t say anything about &quot;non-trivial&quot; programs. In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct.<p>One straightforward way to do this is with a language that always halts. The proof assistant Coq is based on such a language, and it&#x27;s powerful enough to write a C compiler: <a href="http:&#x2F;&#x2F;compcert.inria.fr&#x2F;" rel="nofollow">http:&#x2F;&#x2F;compcert.inria.fr&#x2F;</a><p>It is certainly correct that you can&#x27;t stuff an arbitrarily vexatious program through a proof assistant and get anything useful on the other side. But nobody is interested in proving things about arbitrarily vexatious programs; they&#x27;re interested in proving things about programs that <i>cooperate with the proof process</i>. If your program doesn&#x27;t want to cooperate, you don&#x27;t need an exact answer; you might as well just say &quot;No, I don&#x27;t care, I&#x27;m not trusting you.&quot;