Right. The interesting thing to me about this is its application to proving theorems, especially about programs. Historically, most people interested in having machines prove theorems have looked for algorithms — "proof procedures", the mathematicians call them, and of course they like to prove theorems about these procedures, such as that they're sound (never generate an incorrect proof) and complete (can prove any true theorem). Both of these sound like desirable properties, and for restricted domains such as first-order logic, it's possible to have both; but first-order logic is inadequate for reasoning about programs. For this task, we need higher-order logic, to prove invariants by induction, and Turing's proof arguably shows that there can be no sound and complete proof procedure for higher-order logic. We have to give up something, and of course that something is completeness; we can't part with soundness, because incorrect proofs are not useful.

So we have to accept incompleteness, but obviously we want our program-property prover to be able to prove as much as possible. How do we approach that? I don't think we can make much progress approaching it mathematically; I think we have to approach it as an AI problem. That means figuring out how humans manage to be "partial oracles" and doing the same thing as much as we can. It means heuristics, it means pattern matching, it means machine learning.