Don’t know the programming language Scheme? Don’t have to! (Even if you *had* to it would take less than an hour to learn basic syntax).

When I began this blog I intended to make a blog post explaining a formal proof of Turing’s halting theorem (eg. no algorithm can exist which determines whether a computational procedure always halts for every input. For example, a program that took in a number and printed every number greater than that up to 100 would not halt for every number, for obvious reasons). Both Alan Turing, with Turing machines, and Alonzo Church, with the lambda calculus, independently proved the halting problem (“Entscheidungsproblem”). However, both of these proofs require a lot of background explanation, and they’re not the best way to do it anyways.

The best way, I found, was a simple exercise from the textbook, *Structure and Interpretation of Computer Programs. *Here is a construction of the proof:

Suppose we have “a procedure `halts?` that correctly determines whether `p` halts on `a` for any procedure `p` and object `a`.”

Then we write the following procedures:

`(define (run-forever) (run-forever))`

(This is an infinite loop), and then a specially constructed:

(define (try p) (if (halts? p p) (run-forever) 'halted))

Now, imagine that we called the expression `(try try)` and let it run. If `(halts? try try)` evaluates to `true`, signaling that the function `try` halts when called on itself, then `try` runs forever, a contradiction. Similarly, if `halts?` decides that `try` does NOT halt when called on itself, the function halts.

And there you have it – the contradiction! By *reductio ad absurdum*, a function such as `halts?` cannot exist.

This proof by construction can be implemented in any language where functions are first-class objects, such as Python, JavaScript, and many other modern ones (not Java, of course. Java kind of sucks).

And in addition, if you’re ever taking a computer science course which uses *SICP* as a textbook, Exercise 4.15 is answered for you!