People researching program verification for purposes of improving software engineering really are interested in the kinds of mistakes programmers make, like “recursive functions that might be missing a base case or something”. Or like unbounded iteration for which we can prove termination, but really ought to double-check that proof.
Unbounded iteration for which we cannot (currently) prove termination may be of interest to mathematicians, but even a mathematician isn’t stupid enough to attempt to resolve the Zeta function conjecture by mapping the problem to a question about halting computer programs. That is a step in the wrong direction.
And if we build an AGI that attempts to resolve the conjecture by actually enumerating the roots in order, then I think that we have an AI that is either no longer rational or has too much time on its hands.
I suppose I wasn’t precise enough. Actual researchers in that area are, rightly, interested in more-or-less reasonable halting questions. But these don’t contradict our intuition about what halting problems are. In fact, I would guess that a large class of reasonable programming mistakes can be checked algorithmically.
But as far as consequences for there being, hypothetically, a solution to the general halting problem… the really significant result would be the existence of a general “problem solving algorithm”. Sure, Turing’s undecidability problem proves that the halting problem is undecidable… but this is my best attempt at capturing the intuition of why it’s not even a little bit close to being decidable.
Of course, even in a world where we had a halting solver, we probably wouldn’t want to use it to prove the Riemann Hypothesis. But your comment actually reminds me of a clever little problem I once saw. It went as follows:
If someone ever proves that P=NP, it’s possible the proof will be non-constructive: it won’t actually show how to solve an NP-complete problem in polynomial time. However, this doesn’t actually matter. Write an algorithm for solving SAT (or any other NP-complete problem) with the following property: if P=NP, then your algorithm should run in polynomial time.
(the connection to your comment is that even if P=NP, we wouldn’t actually use the solution to the above problem in practical applications. We’d try our best to find something better)
What you mean ‘we,’ white man?
People researching program verification for purposes of improving software engineering really are interested in the kinds of mistakes programmers make, like “recursive functions that might be missing a base case or something”. Or like unbounded iteration for which we can prove termination, but really ought to double-check that proof.
Unbounded iteration for which we cannot (currently) prove termination may be of interest to mathematicians, but even a mathematician isn’t stupid enough to attempt to resolve the Zeta function conjecture by mapping the problem to a question about halting computer programs. That is a step in the wrong direction.
And if we build an AGI that attempts to resolve the conjecture by actually enumerating the roots in order, then I think that we have an AI that is either no longer rational or has too much time on its hands.
I suppose I wasn’t precise enough. Actual researchers in that area are, rightly, interested in more-or-less reasonable halting questions. But these don’t contradict our intuition about what halting problems are. In fact, I would guess that a large class of reasonable programming mistakes can be checked algorithmically.
But as far as consequences for there being, hypothetically, a solution to the general halting problem… the really significant result would be the existence of a general “problem solving algorithm”. Sure, Turing’s undecidability problem proves that the halting problem is undecidable… but this is my best attempt at capturing the intuition of why it’s not even a little bit close to being decidable.
Of course, even in a world where we had a halting solver, we probably wouldn’t want to use it to prove the Riemann Hypothesis. But your comment actually reminds me of a clever little problem I once saw. It went as follows:
(the connection to your comment is that even if P=NP, we wouldn’t actually use the solution to the above problem in practical applications. We’d try our best to find something better)