The statement regarding checking logic in computer programs is not misleading (though of course, your characterization of it is); there are many systems which a

The statement regarding checking logic in computer programs is not misleading (though of course, your characterization of it is); there are many systems which are not subject to the halting problem in fact (at least in any way that affects practice ---> You can simply limit constructible terms to those which provably terminate, if you please). Statements like yours about Turing & Gödel are a common mistake. You don't have to _decide_ whether a program halts in order to prove it. In many cases, termination is not so much even a proof obligation as it is a _fact_ by construction; in the harder case where termination is not obvious structurally, you can simply rewrite your general recursion as a call-graph, and then termination is a proof obligation which you must satisfy if you wish to execute it. Decidability is much a much stronger thing than "provability in most relevant cases", and it turns out that the latter suffices. By Gödel, there are indeed "true" sentences which you cannot prove in a particular system, but I am willing to give you a hundred thousand dollars if you can actually find one and print it out. That is, Gödel's result was indeed sort of constructive, in that it did provide a scheme to construct such a sentence, but nobody does so because the term is so unfeasibly large. There are many things which we should like very much to be decidable, some of which _can_ in fact be decidable (by Turing, termination is not one of those). For instance, in some systems (such as Intensional Type Theory), type checking is decidable, which is really nice. In others, type checking is undecidable (such as in Extensional Type Theory); does this mean that type checking cannot be done? Of course not. It simply means that type checking becomes a proof obligation, since the typing derivations may not be entirely synthesized by the type checker. (A simple demonstration of this is equality in a NuPRL-like system: propositional equality is reflected into definitional equality; there is not decidable equality for functions; therefore, there are equations which might hold definitionally by equality reflection, but for which further proof would be required; therefore, definitional equality is undecidable; therefore type checking is undecidable; but we can still prove that a term is well-typed, even if type checking is undecidable.)