Rice's theorem in plain wordsWhy no check works on every program and what to do about it

The point: what Rice's theorem rules out

Rice's theorem says that all non-trivial semantic properties of programs are undecidable. Henry Gordon Rice proved it in his 1951 dissertation. The whole theorem sits in three words of that statement.

However clever the check, there is a program on which it answers wrongly.

How to read this in everyday terms. Imagine a checker who is handed any program and asked: “Will it ever charge money without an order?” The checker can be as clever as you like, work as long as you like and know every programming language. The theorem says there is still a program on which it answers wrongly or never answers. This is a property of the task itself, and improving the checker doesn't lift it, just as improving a design doesn't produce a perpetual motion machine.

It matters what the theorem leaves allowed. The ban covers one combination: “any program” plus “an exact yes or no” plus “a behavioural property”. Remove any one part and checking becomes possible again.

Predicate: a question about the text or about behaviour

A predicate is a yes-or-no question about a program. There are two kinds, and Rice's theorem concerns only the second.

The code is the same. The difference is what you must look at to answer: a finite text or an infinite number of runs.

Why the word “semantic” is key here. A semantic property depends only on what the program does and not on how it is written. If two programs behave the same on every input, they get the same answer to a semantic question. Example: one program sums purchases with a loop, another with a library function. The texts differ, the behaviour is the same, and “can the sum be negative” has one answer for both. But “does the code contain a loop” has different answers, because it is a question about the text.

A close analogy is the imperative and declarative approaches. Code writes down steps, the “how”, while a rule about the result is a statement, the “what”. Rice's theorem says that in general you can't mechanically derive from the steps whether the statement about the result holds. A caveat: in a powerful declarative language behaviour can't be checked from the text either. Exact answers come from poor notations such as a database constraint, whose behaviour is visible in the notation itself.

The proof on one example

Checking the rule for $Q$ would tell whether $P(w)$ halts, and no program answers that.

The idea of the proof is a reduction. If one task could be solved, so could another that is already known to be unsolvable. So the first is unsolvable too. Here the first task is checking a behaviour rule and the second is the halting problem.

Take any program $P$ with input $w$ and build a new program $Q$ from it:

Step $B(x)$ breaks the rule, while a program that runs forever does not. So $Q$ reaches the breach only if $P(w)$ ever finishes:

If a check of the rule existed for every program, then given $Q$ it would also answer whether $P(w)$ halts. But Alan Turing proved that no program answers that question, the halting problem. So there is no universal rule check either. The rule can be anything: any non-trivial behavioural property fits in place of “money without an order”.

The same steps in order:

1. Take any non-trivial behaviour rule. Since it is non-trivial, some program breaks it. The part of that program which breaks the rule is step $B$.
2. Take any program $P$ and its input $w$ for which the question is whether $P(w)$ halts.
3. Glue $Q$ together: first $P(w)$, then $B$. The gluing is a simple mechanical procedure you could write in a minute.
4. Hand $Q$ to the imagined universal check. Its answer “breaks” means “$P(w)$ halted”, and “doesn't break” means “didn't halt”.
5. That is a solution to the halting problem, which doesn't exist. So the universal check doesn't exist either.

One caveat for precision. The construction assumes that a program which runs forever and does nothing doesn't break the rule. If that isn't so for some rule, take the opposite rule: checking it is no easier, and the argument repeats word for word.

Where the trick comes from: the halting problem and the barber paradox

Rice's theorem reduces any behaviour check to the halting problem and so inherits its undecidability. The halting problem in turn is proved with a trick over a hundred years old: a question about itself.

The contrarian asks the judge about itself and does the opposite, so the judge is wrong whatever it says.

Suppose there is a judge that says, for any program, whether it halts. Write a contrarian program: it asks the judge about itself and does the opposite. If the judge says “halts”, the contrarian loops forever; if it says “won't halt”, the contrarian stops at once. The judge is wrong either way, so it can't exist.

The barber shaves everyone who doesn't shave themselves. He himself fits into neither of the two sets.

The same trick sits in the barber paradox, a vivid version of Russell's 1901 paradox. The villagers split into set $A$, those who shave themselves, and set $B$, those the barber shaves, and everyone is in exactly one. The barber has no place: in $A$ he ends up in $B$, in $B$ he ends up in $A$. Russell has the same about sets: $R = {x : x \notin x}$, and $R \in R \iff R \notin R$.

Why a question about itself is so strong. A program is text too, so it can be fed to another program and even to itself. As soon as a checker can speak about any program, it must also speak about a program that asks it about itself and does the opposite. Then any answer it gives is wrong. The same move appears in the barber paradox, Russell's paradox and Gödel's incompleteness theorem.

What to do: three frames inside which the answer is exact

The theorem rules out a check for every program. For programs inside a frame a check is possible.

The theorem bans one combination of three conditions at once: the check must work for any program, on any behaviour question, and answer exactly “yes” or “no”. The proof relies on all three: it builds a program $Q$ the check must accept, asks a behaviour question about it, and demands a definite answer. Each way removes one condition, and the proof stops working.

Each of the three answers is exact only within its limits. The search proves the rule holds in a model with 3 rooms and 5 bookings, not in the production database with thousands of bookings. The code search proves there is no write around the rule, not that the database constraint itself is written correctly. A “holds” answer is exact, but some edits still go to a person. So the ways are used together: the model checks the design before code, the constraint and the search check the code itself, and a person looks at whatever is left with a label.

Any check that works inside a frame makes errors of two kinds. It helps to decide in advance which one you can live with.

For rules about money and access, choose checks that raise false alarms but never miss a breach: a database constraint, type checking, a single writer per table. A developer clears an extra label in a few minutes, while a missed double charge comes back as a customer complaint and a refund.

In DDD terms it looks like this. The bounded context “Booking” talks only about rooms, bookings and time: it has no words like “payment” or “notification”. The rule “bookings never overlap” concerns one table, and one aggregate, “Booking”, writes to it. So “can the code break the rule” reduces to a text question: does anything other than the aggregate write to that table. That is the narrow language: the context's vocabulary is small, each word has one meaning, and the rule is checked by search. That is why the aggregate border is a convenient place for a check.

The link to the CAP theorem: a common core, different reasons

The CAP theorem is a well-known ban from distributed systems. When data lives on several servers and the link between them breaks, the system can't both answer every request and show everyone the same data. It has to choose: wait for the link to return, or answer from its own copy, which may be stale. Eric Brewer stated this in 2000; Seth Gilbert and Nancy Lynch proved it in 2002.

The common core. In both bans: while an event hasn't happened yet, you can't tell whether it will happen later or never, however long you wait. A server doesn't know whether a neighbour's message is lost or just late. A program check doesn't know whether the program will finish in a billion steps or never. While the waiting time is unbounded, both have exactly two ways out, and only one of them can be chosen: wait or answer now.

The top of the diagram is a fork between two mutually exclusive ways out. The bottom is a third path: it changes the condition that created the fork.

What the two branches of the fork look like in a network and in a program check:

The third path: bound the time. It removes the fork itself. If a message in the network is known to take no longer than 2 seconds, the server waits 2 seconds and then knows for sure: the message is lost. The answer both comes and is right. Programs are the same: if a language or model guarantees every program finishes within a known number of steps, the check runs it to the end and answers exactly. That is how the small world and the narrow language from the previous section work. The price is that the bound must be ensured in advance: a network with a guaranteed delay and a language in which an endless loop can't be written.

Different reasons. A CAP server lacks information: even an infinitely clever server can't learn what happens at its neighbour beyond the broken link. A program check has the information, the whole code is in front of it, but the answer can't be computed from that code. These are different kinds of impossibility, so Rice's theorem and CAP are not the same thing.

How strict this is. Both halves are established: Rice's theorem and the CAP proof are published. Matching the ways out is the author's observation; there is no single theorem for both cases. Brewer himself later warned that the “two of three” formula oversimplifies: in reality it is a scale, and the choice arises only during a partition. Checks are the same: what matters is how often a check says “don't know” or is wrong.

Frequently asked questions