Skip to main content

Can Code Check Itself? What the Halting Problem, Rice's Theorem and Gödel Actually Say

· 16 min read
Pere Pages
Software Engineer
A small robot at a desk holds up a hand mirror. Inside the mirror, frames repeat smaller and smaller around a question mark. Blocks of code float around the robot.

People often say that computer science "proves" a program cannot check itself. That is not quite what the theory says: a program can read its own code without any problem, but no program can decide, with certainty and for every possible program, what that program will do.

Two different questions​

There are two questions that sound the same but are not.

The first question is: can a program look at its own code? The answer is yes. A program can open its own source file, print it, count its lines, or search it for a word. There is even a famous kind of program that prints its own code without opening any file.

The second question is: can a program always decide, correctly, what any program will do when it runs? For example: "Will this program ever stop?", "Will this function ever return zero?", "Is this code free of bugs?". Here the answer is no. There is no general method that gives the right answer for every program. This is not because our computers are too slow or our tools are too new. It is a mathematical limit, proved in the 1930s.

So the limit is not "a program cannot look at itself". The limit is "no program can decide, in general, how programs behave". The rest of this post shows where that limit comes from and what it means for the tools we use every day.

The halting problem: will this program ever stop?​

The best-known result is about one question: does a program stop, or does it run forever? This is called the halting problem ("to halt" means "to stop").

In 1936, Alan Turing proved that no program can answer this question correctly for every program and every input[1]. Note the word every. For many single programs the answer is easy. A program with no loops and no recursion (no function that calls itself) always stops. A program that is just while True: pass never stops. The theorem says something different: there is no single method that works for all programs.

The proof uses self-reference: a program that asks a question about itself and then does the opposite of the answer. Here is the idea in Python. First, imagine that someone gives us a perfect function halts. It takes the code of a program and some input, and it always answers correctly, in a finite time, whether that program stops on that input:

def halts(program, data) -> bool:
"""Imagine this always returns the correct answer, and always returns."""
...

Now we use halts to write a second function. It asks halts what a program does when the program receives its own code as input, and then it does the opposite:

def troublemaker(program):
if halts(program, program):
while True: # "halts" said it stops, so we loop forever
pass
else:
return # "halts" said it runs forever, so we stop at once

Finally, we give troublemaker its own code: troublemaker(troublemaker). Follow both possible answers:

  • If halts says "it stops", then troublemaker enters the endless loop. So it does not stop, and halts was wrong.
  • If halts says "it runs forever", then troublemaker returns at once. So it stops, and halts was wrong again.

Both answers are wrong, so the perfect halts cannot exist. The problem is not that the program looked at itself; the problem is that a perfect halts would have to predict a program built to do the opposite of its prediction. The Stanford Encyclopedia of Philosophy gives the same argument with Turing machines (Turing's mathematical model of a computer)[2].

Rice's theorem: what code does, not how it is written​

The halting problem is about one question. In 1953, Henry Gordon Rice showed that the same limit applies to almost every interesting question about programs[3].

To understand Rice's theorem, we need to separate two kinds of questions about code:

  • Questions about how the code is written (its syntax, the text and its structure). "Does this file use the word eval?" "Is this function longer than 50 lines?" "Is every bracket closed?" A program can answer these by reading the text. They are always decidable, which means a program can always give the correct yes-or-no answer.
  • Questions about what the code does when it runs (its semantics, its behaviour). "Does this function ever return zero?" "Can this code divide by zero?" "Does this program ever send a password over the network?" "Does this function sort its input correctly?"

Rice's theorem says: every question about what a program does is undecidable, unless the answer is the same for all programs. "Undecidable" means that no program can give the correct answer for every possible program. Questions with the same answer for every program tell us nothing, so in practice every useful question about behaviour is undecidable.

Question about codeKindCan a tool always answer it correctly?
Does the file contain the word eval?How it is writtenYes
Is every bracket closed?How it is writtenYes
Does this function ever return zero?What it doesNo, not in general
Can this code divide by zero?What it doesNo, not in general
Is this program free of bugs?What it doesNo, not in general

Why is this true? Because if you could answer any of these questions perfectly, you could also answer the halting problem. Take the question "does this function ever return zero?". Suppose we had a perfect tool that answers it. Now take any program P and any input x, and write this small wrapper:

def wrapper(n):
P(x) # run the program we want to ask about
return 0 # we only reach this line if P(x) stops

wrapper returns zero if, and only if, P(x) stops. So if our perfect tool could tell us "wrapper returns zero", it would also tell us "P(x) stops". That would solve the halting problem, which we already know is impossible. So the perfect "returns zero" tool cannot exist either.

The same trick works for any question about behaviour: put "first run P(x)" in front of the behaviour you are asking about. (Strictly, Rice's theorem is about what a program returns for each input. Questions about what happens during the run, such as "can this code divide by zero?", are not covered by the theorem itself, but this trick shows they are undecidable for the same reason.) So no checker can be both always correct and fully general about what code does, and that includes a checker that checks its own code.

Gödel: the same limit in logic​

Five years before Turing, in 1931, the mathematician Kurt Gödel found a very similar limit in logic. His work is about formal systems: sets of basic rules (called axioms) from which you prove mathematical statements step by step.

Gödel proved two incompleteness theorems. The first says that any consistent formal system strong enough to describe ordinary arithmetic contains true statements it cannot prove. ("Consistent" means it never proves both a statement and its opposite.) The second says that such a system cannot prove its own consistency.[4]

The proof uses the same kind of self-reference as Turing's. Gödel built a statement that says, in effect, "this statement cannot be proved in this system". If the system could prove it, the system could also show that the statement can be proved, and so it would contradict itself. So, if the system is consistent, the statement cannot be proved, and that is exactly what the statement says, so it is true.

The parallel with programs is close:

Logic (Gödel, 1931)Programs (Turing, 1936)
The thing being checkedA formal systemA program
The self-referring object"This statement cannot be proved"troublemaker(troublemaker)
What it cannot doProve all true statements, or prove its own consistencyDecide, for every program, whether it stops

Note what the second theorem does not say. A stronger system can still prove that a weaker one is consistent. The limit is about a system proving this one thing about itself, with only its own rules. For programs, the situation is similar: one tool can check a specific other program with extra help, but no tool can decide everything about all programs, its own code included.

A program can still look at itself​

After so much "impossible", it is important to come back to the first question: can a program look at its own code? Yes, and there is a theorem that guarantees it.

In 1938, Stephen Kleene proved what is now called Kleene's recursion theorem[5]. In plain words, it says that a program can always get a copy of its own code and then do whatever it wants with that copy: print it, count it, analyse it, or pass it to another program. It does not need to read its source file from the disk. The self-reference that made troublemaker possible is not a trick that breaks the rules; it is always available.

The best-known example is a quine: a program that prints its own source code exactly, without reading any file. Here is a quine in Python. Its output is exactly these two lines:

s = 's = %r\nprint(s %% s)'
print(s % s)

How it works:

  1. The variable s holds a template of the whole program, with a hole (%r) where the template itself should go.
  2. s % s fills the hole with s, written as a Python string literal (%r adds the quotes and the \n). The %% in the template becomes a single %.
  3. The result is the full program text, which is then printed.
So the limit is not about looking at yourself, which is always possible; it is about deciding, with certainty and for every program, what code will do.

In practice: every checker is an approximation​

If no tool can decide what all code does, how do linters, type checkers and static analysers work? (A linter checks code for style problems and common mistakes. A type checker checks that values are used with the right types, for example that you never add a number to a list. A static analyser looks for bugs by reading code without running it.)

They work because they give up on being perfect. Rice's theorem leaves three options, and each tool picks one or mixes them:

  1. Raise false alarms. The tool warns about every real problem of the kind it checks, but it also warns about some code that is actually fine. Such a tool is called sound: it never misses a real problem, but it can give false positives (warnings about code that is correct).
  2. Miss some problems. The tool only warns when it is sure, so every warning is real, but some real problems pass without a warning. Such a tool is called complete: it never gives a false alarm, but it can give false negatives (missed bugs).
  3. Answer "I don't know". The tool gives up on some programs, for example after a time limit, or asks a human for help.

Real tools show all three choices. The Rust compiler, for example, picks false alarms on purpose for memory safety (never reading or writing memory that the program should not touch). The part of the compiler that checks this is called the borrow checker. The Rust book explains that "static analysis is conservative" and that "it's better for it to reject some valid programs than to accept some invalid programs"[6]. TypeScript goes the other way: its design goals list a "sound or provably correct type system" as a non-goal, because the team chose a balance between correctness and productivity[7]. So TypeScript accepts some programs that fail with a type error while they run.

In industry, false alarms are often the bigger problem. A team at Google that built static analysis tools found that developers stop trusting and using tools that give many false positives[8]. Many practical tools are therefore "mostly sound" on purpose: sound in most places, and unsound in a few well-known places to keep false alarms low. Researchers call this soundiness[9].

Testing is an approximation too, of the "miss some problems" kind. A failing test shows a real bug, but a passing test suite does not show that there are no bugs. The computer scientist Edsger Dijkstra wrote in his Notes on Structured Programming: "Program testing can be used to show the presence of bugs, but never to show their absence!"[10]

Linter rules about how code is written, such as "never use eval", can be exact, because they ask a question about the text. Linter rules that try to find bugs are approximations, like the other tools in this table.

ToolMain choiceNever misses problems of its kind?Never gives false alarms?
Rust borrow checker (memory safety)False alarmsYes, in safe Rust codeNo
TypeScript type checkerBalance, unsound by designNoNo
Linter rules that try to find bugsPatterns in the text, plus guessesNoNo
TestsMisses some problemsNoYes, if the test is correct
Formal proof, written with human helpAsks a humanYes, for the proved propertyYes

The last row does not break Rice's theorem. A formal proof (a mathematical proof that a specific program has a specific property, checked by a computer) works for one program at a time, and a human writes most of the reasoning. Rice's theorem only forbids a tool that decides automatically and for every program.

So the right question for any checker is not "is it perfect?" but "which mistakes did it choose to make?".

What this means for code review, by humans and by AI​

The theorems are about programs, so they apply directly to every automated reviewer: tests, static analysers, and an artificial intelligence (AI) model that reviews a pull request (a proposed change to the code). None of them can decide correctly, for every program, what code does. The theorems do not prove the same limit for human reviewers, but in practice humans are approximations too: they miss some bugs, raise some false alarms, or both.

This also tells us what the theorems do not say. They do not say that code reviewed by the same person or model that wrote it is worse than code reviewed by someone else. The limit is about deciding behaviour in general, and it is the same for every automated reviewer. If self-review is weaker in practice, the reason is a different one: the author and the reviewer have the same gaps in what they notice, so they tend to miss the same mistakes. That is a practical observation about people and models, not a result from Turing or Rice.

The practical lesson follows from the previous section. Because each check is imperfect in its own way, the useful approach is to combine checks that fail differently: a type checker that rejects some correct code, tests that miss some bugs, a linter for known patterns, and a reviewer who did not write the code. No single checker, and no program checking itself, can give certainty; several different imperfect checks together catch much more than any one of them.

References​

  1. Alan M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem — Proceedings of the London Mathematical Society, 1936
  2. Turing Machines, § The halting problem — Stanford Encyclopedia of Philosophy
  3. H. G. Rice, Classes of Recursively Enumerable Sets and Their Decision Problems — Transactions of the American Mathematical Society, 1953
  4. Gödel's Incompleteness Theorems — Stanford Encyclopedia of Philosophy
  5. Kleene's recursion theorem — Wikipedia
  6. Unsafe Rust — The Rust Programming Language
  7. TypeScript Design Goals — Microsoft TypeScript wiki
  8. Caitlin Sadowski et al., Lessons from Building Static Analysis Tools at Google — Communications of the ACM, 2018
  9. Benjamin Livshits et al., In Defense of Soundiness: A Manifesto — Communications of the ACM, 2015
  10. Edsger W. Dijkstra, Notes on Structured Programming (EWD249)