Turing kicked us out of Heaven

The halting problem is why we can't have nice things.

The halting problem is "undecidable": there's no algorithm which can tell you if an arbitrary program with an arbitrary input will halt or not. IE, if you give me a proposed "halt-detector", I can inspect it and come up with a program and input for which it would give the wrong answer.

Most people think that's a cool mathematical theory but don't know the real world relevance, because computers aren't Turing machines and have finite memory, so all programs are guaranteed to halt. I once saw a keynote speaker say their programming language was stronger than Turing-complete because all programs in it had a timeout, and so they solved the halting problem.

To better understand why the halting problem is so important, it's better to look at what the world would be like if it was solvable.

A recursively enumerable problem is a boolean problem where any true answer can be determined in a finite time. We can come up with an algorithm that, if the answer is "true", halts and returns "true", and if the answer is "false", either returns "false" or runs forever. Here's a recursively enumerable problem:

def sum_of_two_primes(num):
    for p1 in range(2, num):
        for p2 in range(2, num):
            if is_prime(p1) and 
               is_prime(p2) and 
               p1 + p2 == num:
                return True
    return False

x = 4
while sum_of_two_primes(x):
    x += 2

This algorithm runs until it finds an even number that's not the sum of two primes, then halts. Goldbach's Conjecture, one of the oldest unsolved problems in all of mathematics, says that there's no such number. This algorithm halts iff Goldbach's conjecture is false.

If the halting problem was solvable, then anyone with a computer could prove Goldbach's conjecture in an afternoon.

This is also why "all computers halt anyway" doesn't really "solve" the halting problem. Let's say the computer has finite memory, so there's a largest integer that can be stored without crashing. Our algorithm then looks like this:

while sum_of_two_primes(x) and x < 999_999_999_999_999:
    x += 2

Yeah sure this program always halts, but it's no longer checking Goldbach's conjecture. It only checks it up to a certain number! The original algorithm was useful because it could potentially run forever, and capping the runtime takes that property away. It's no longer interesting to us.

A huge number of unsolved math problems are recursively enumerable: odd perfect numbers, the ABC conjecture, the Riemann hypothesis, P vs NP, etc. If there existed a halt detector then we could shove mathematics centuries into the future.¹ But the halting problem is provably undecidable, so we live in a very different world.

About that P vs NP

This is a very rough sketch of how you'd do it:

First, write a bash script P1 that runs a SAT solver on every possible SAT problem and halts if any of them take exponential time. You don't actually have to run P1, just call HALTS(P1, Solver) to see if the solver solves all problems in polynomial time.

Then, make P2 enumerate all strings and calls HALTS(P1, str) on them. If P1 halts (or errors), then str was not a polynomial-time SAT solver, so move onto the next string. If P1 halts, have P2 halt. Then HALTS(P2) is true iff there is some SAT solver which solves all SAT problems in polynomial time, ie HALTS(P2) <=> P = NP.²

(You'd have to figure out how to check if a specific problem took exponential time, but that's a lot easier than proving all of P vs NP!)

Programmers would be a lot better off too

You're reviewing PR for a completely unfamiliar codebase. You see that pure function f has been refactored into f', and want to check that the two give identical outputs on every input. With a halt detector, that's trivial:

1. Write program EQL(f, g) that iterates through all possible inputs and checks that f(x, y, z) == g(x, y, z).
2. Call HALTS(EQL, f, f').

Now, in our world, this is impossible. In fact, we can prove there's no program EQL that can check if two arbitrary functions are identical. Let's say EQL(f, g) did exist. Then define HALTS(p, args) like this:

def HALT(p, args):
    def q:
        p(args)
        return iden # some function
    return EQL(q, iden) 

Now HALT returns true iff q returns iden, which happens iff p halts, meaning we've bootstrapped a halt detector, which we already know is impossible.

Is this again made uninteresting if we assume finite memory. p always terminates so q always returns iden so HALT always returns true, as all programs terminate. But at the same time, HALTS(EQL, f, g) no longer tells us if f and g are equal, only that they are for a subset of inputs. That's just property testing!

The more general version of this is Rice's theorem: determining any non-trivial semantic property of a program is undecidable. So no perfect optimization tools, no perfect bug finders, no perfect backwards-compatibility checkers. Again, this is in the general case, where we have to come up with an algorithm that works for all programs and inputs. In the specific case, say in a specific domain with specific classes of inputs, this can be possible. But it'll require a lot more time and effort than you'd need if you just had a halt-detector.

tl;dr

If the halting problem was decidable, we'd be able to trivially prove a huge class of theorems, solve a huge class of numerical problems, and make our lives as programmers way way easier. But it's undecidable, so we can't. We're stuck programming on earth.

Model Mondays tonight!

Short notice, I know, but I'll be a guest at Marianne Bellotti's Model Monday tonight! Marianne's a cool friend of mine and is currently working on the Fault modeling language. The talk starts at 7 PM Central time and will probably be about modeling in TLA+, but who knows where it will actually go.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.