> That's why Turing / Gödel results really tell something fundamental about computing/proving; it tells everyone that they do not need to spend time solving an unsolvable problem on computers "as we know them"
Consider something like Turing's proof that the halting problem is undecidable – does that have practical relevance, even just in telling us that there is no point in trying to solve an unsolvable problem?
That's the standard line but I doubt it. The thing is, the halting problem is practically irrelevant; what has practical relevance is the bounded halting problem. Practically, you don't care about the difference between a program that never halts, and a program that halts after a googolplex steps, but that distinction is essential to the halting problem as defined. And, the practically relevant, bounded halting problem, is in fact decidable. Now, it is still intractable, because it is EXPTIME-complete, and we also know (per the time hierarchy theorem) that EXPTIME-complete problems are not in P.
So Turing's proof doesn't actually tell us anything much useful about whether the halting problem is solvable in practice, whereas the proof that the bounded halting problem is EXPTIME-complete does. Suppose (counterpossibly) that the bounded halting problem was in P instead of EXPTIME-complete; then the halting problem might actually be tractable in practice, even though Turing's proof of the unbounded halting problem's undecidability would still hold.
The undecidability of a specific formulation of the halting problem is practically irrelevant, but you should never take published results too literally. If the halting problem is undecidable in one formalism, it is also undecidable in many other formalisms, and so is a wide class of other problems that can be reduced to the halting problem.
Rice's theorem is one immediate consequence of the undecidability of the halting problem. It effectively states that if you are writing code that analyzes (certain external behavior of) other code, there will always be edge cases your code cannot handle. It is useful to understand that the perfect algorithm is not out there, just waiting to be discovered. Instead of searching for it, you should start thinking about the trade-offs between resource usage and the ability to handle increasingly rare edge cases.
I'm not a fan of resource-bounded variants of decision problems, because the standard complexity classes are ugly beasts. Reasoning about them is so difficult that many fundamental problems remain unsolved. And even if you manage to prove something, the excessive use of quantifiers means that you only learn something about the worst-case behavior with some arbitrarily large inputs.
The resource-bounded problems also miss the point. Impossibility results are not really about the impossibility of proving something with realistic or unrealistic resources. The proof ideas are often more important than the results. One idea is particularly simple: if you have already written your code, I can write an input that fools it.
> Rice's theorem is one immediate consequence of the undecidability of the halting problem.
I wonder if one could construct a bounded analogue of Rice's theorem? Something like "all non-trivial, semantic properties of programs that use maximum resources R are undecidable by programs using maximum resources R".
> I'm not a fan of resource-bounded variants of decision problems, because the standard complexity classes are ugly beasts. Reasoning about them is so difficult that many fundamental problems remain unsolved.
It seems to be that, reasoning about actual computers is harder than reasoning about physically impossible theoretical ones, so people would prefer to study the later than the former. Fair enough, but surely the former study is more practically relevant – even if harder – than the later; and I don't know why in the later the study of one particular class of physically impossible machines (Turing-equivalent machines) gets privileged over the study of other more powerful classes of physically impossible machines (such as oracle machines, or supertask machines). All physically impossible machines are equally physically impossible.
(Privileged not in the sense of being ignored – of course there is a great deal of theoretical work done on super-Turing computation; but privileged in the sense that super-Turing computation is often presented as something only of interest to specialists, whereas work on Turing-equivalent computation gets promoted as something of practical relevance and general interest.)
> One idea is particularly simple: if you have already written your code, I can write an input that fools it.
Here's a very similar idea about computation with bounded resources: If you had a perfect program analysis program that only worked for programs consuming up to some resource limit R, then it would require more than R to apply the same analysis to itself.
And either idea may not be true for dialetheic machines [0]. Dialetheic machines are, as far as we know, not physically realisable; but Turing machines aren't either.
You are saying that the decision problem of "Is this algorithm A in P?" is undecidable for arbitrary algorithms A. We don't need a general solution to that decision problem to be able to prove that some particular algorithm is or isn't in P; just like how, we don't need a general solution to the halting problem to prove some particular program does or doesn't halt. The halting problem only means we can't have a computable procedure which will generate such a proof in every case.
The fact that we've actually proven the bounded halting problem is not in P doesn't contradict this. The undecidability of determining whether any arbitrary problem is or isn't in P doesn't prevent us from having a proof that some particular problem is or isn't.
And I said counterpossibly that if the bounded halting problem were in P not EXPTIME-complete, then the halting problem might be practically solvable even if Turing's proof of the undecidability of the unbounded halting problem still held. In this counterpossible, we don't need to be able to solve the decision problem of determining whether an algorithm is in P, all we need is a proof that this one particular algorithm is in P. The undecidability of the decision problem in general tells us nothing about whether we could know its answer for individual cases.
Consider something like Turing's proof that the halting problem is undecidable – does that have practical relevance, even just in telling us that there is no point in trying to solve an unsolvable problem?
That's the standard line but I doubt it. The thing is, the halting problem is practically irrelevant; what has practical relevance is the bounded halting problem. Practically, you don't care about the difference between a program that never halts, and a program that halts after a googolplex steps, but that distinction is essential to the halting problem as defined. And, the practically relevant, bounded halting problem, is in fact decidable. Now, it is still intractable, because it is EXPTIME-complete, and we also know (per the time hierarchy theorem) that EXPTIME-complete problems are not in P.
So Turing's proof doesn't actually tell us anything much useful about whether the halting problem is solvable in practice, whereas the proof that the bounded halting problem is EXPTIME-complete does. Suppose (counterpossibly) that the bounded halting problem was in P instead of EXPTIME-complete; then the halting problem might actually be tractable in practice, even though Turing's proof of the unbounded halting problem's undecidability would still hold.