I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist).
Of course, if the program did eventually terminate, then a termination proof would exist (just enumerate all the state transitions, there's only a finite number of them). So what it means is that some programs never halt, but it's impossible to prove this fact.
This ties in with Gödel's theorems, e.g. (if we use ZFC and assume ZFC is consistent) a program that enumerates all possible valid proofs from axioms in ZFC and halts whenever it finds a contradiction, would never halt, but we can't prove this (at least not in ZFC) because that would contradict Gödel's second incompleteness theorem.
Comments
I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist).
Of course, if the program did eventually terminate, then a termination proof would exist (just enumerate all the state transitions, there's only a finite number of them). So what it means is that some programs never halt, but it's impossible to prove this fact.
This ties in with Gödel's theorems, e.g. (if we use ZFC and assume ZFC is consistent) a program that enumerates all possible valid proofs from axioms in ZFC and halts whenever it finds a contradiction, would never halt, but we can't prove this (at least not in ZFC) because that would contradict Gödel's second incompleteness theorem.