Rice's Theorem

Symptom

The security team asks for a scanner with no false positives and no false negatives. Every piece of malware caught, nothing legitimate quarantined.

The platform team asks whether the analyzer can flag every function that performs I/O, so the pure ones can be cached automatically.

Somebody in review asks why the compiler cannot just eliminate all the dead code, given that it clearly eliminates some.

You have already met the answer for one property: termination is undecidable (T010). What is not obvious, and what makes this the result that actually governs your working life, is that termination was not special. Every one of these questions is undecidable, and so is nearly every question of that form you will ever be asked, and there is a single theorem that says so without requiring you to construct a proof each time.

Statement

Every non-trivial semantic property of programs is undecidable.

Two words are load-bearing, and almost every misapplication of this theorem is a failure to check one of them.

Semantic means the property is about the function the program computes, not about its text. Formally, if $P$ and $Q$ compute the same function, then $P$ has the property exactly when $Q$ does. “Halts on every input” is semantic. “Contains the substring eval” is not, and neither is “is under 100 lines” or “has more than three nested loops.”

Non-trivial means some program has the property and some program does not. “Is a program” is trivial (all of them). “Computes a function no program computes” is trivial (none of them). Everything else is non-trivial, which is to say: everything interesting.

Read the quantifier carefully, because it is unusually strong. This is not “some properties are undecidable.” It is: pick any semantic property at all, at random, sight unseen. If it is not trivial, it is undecidable. There are no interesting exceptions, and you do not have to search for a proof.

Argument

We reduce from halting. Assume a decider $R$ for the property $\mathcal{P}$, and build from it a decider for HALT, which T010 forbids.

Let $\varnothing$ denote the everywhere-undefined function — the one computed by a program that loops on every input. Without loss of generality, assume $\varnothing \notin \mathcal{P}$. (If it is in $\mathcal{P}$, run the whole argument on the complement property, which is also semantic and non-trivial, and is decidable exactly when $\mathcal{P}$ is.)

Since $\mathcal{P}$ is non-empty, pick some $f \in \mathcal{P}$, computed by a program $F$.

Now, given an arbitrary program $P$ and input $x$ — the halting question we want to answer — construct this program:

def M_Px(y):
    run P on x          # ignore the result; may never return
    return F(y)         # only reached if the line above returned

Building M_Px from P, x, and F is pure text manipulation. No execution. It always succeeds, and it terminates, because writing a program is not running it. This step is the one worth slowing down on: we are not asking whether M_Px halts, only writing it down.

What function does M_Px compute?

• If $P$ halts on $x$, the first line returns and M_Px(y) = F(y) for every $y$. So M_Px computes $f$, which is in $\mathcal{P}$.
• If $P$ does not halt on $x$, the first line never returns, so M_Px(y) is undefined for every $y$. So M_Px computes $\varnothing$, which is not in $\mathcal{P}$.

So M_Px has property $\mathcal{P}$ if and only if $P$ halts on $x$.

Now run the decider we assumed exists:

def Halts(P, x):
    return R(build_M(P, x))

That is a total, always-correct decider for the halting problem. T010 says there is none. So $R$ does not exist. $\blacksquare$

Notice what the proof never did: it never looked at what $\mathcal{P}$ is. The argument works for “computes a total function,” “always returns 0,” “is equivalent to this reference implementation,” “never writes to the network.” The property is a black box, which is precisely why the theorem covers all of them at once. Undecidability here is not a fact about any particular property; it is a fact about the fact that programs can be composed.

Cohen’s corollary: perfect virus detection is impossible. Fred Cohen ran this argument in 1987 with $\mathcal{P}$ = “propagates itself,” and got the result the antivirus industry has lived under ever since. The neat version is a direct diagonal, and it is worth seeing because it needs no reduction at all. Suppose is_virus(P) is a perfect detector. Write:

def V():
    if not is_virus(V):   # ask the detector about myself
        infect()          # ... and if it says I'm clean, infect

If is_virus(V) says clean, V infects, so it was a virus and the detector was wrong. If it says infected, V does nothing at all, so it was clean and the detector was wrong. Same structure as D in the halting proof, and it explains the industry’s shape: signatures (unsound, miss new malware), heuristics (false positives), sandboxing (bounded, so evadable by waiting). Those are not three competing products. They are the three concessions the theorem leaves available.

Forbids

A perfect optimizer. “Is this code dead?” is semantic and non-trivial, so no compiler eliminates exactly the dead code. Every optimizer is conservative: it removes what it can prove is dead and leaves the rest.

A perfect equivalence checker. “Does $M$ compute the same function as this reference?” is the property “computes $f$”, non-trivial and semantic. So no tool decides whether your rewrite preserved behaviour. This is why refactoring is tested rather than proved, and why superoptimizers work over tiny fragments.

A sound and complete effect checker. “Is this function pure?”, “does it ever touch the filesystem?”, “can it throw?” — all semantic. Any language that tracks effects does it by making programmers declare them in types, converting a semantic question into a syntactic one, which is the only move available.

Perfect malware detection, per Cohen, and by the same argument perfect detection of any behavioural class: cryptominers, exfiltration, ransomware.

A perfect security auditor. “Does this program ever leak the secret key?” is semantic. Whatever your audit does, it is not this.

Does not forbid

It does not forbid type systems, and the “Rice’s theorem says static analysis is impossible” line is the single most damaging misuse of a theorem in this series. It shows up in real code review to reject real tooling. But look at what the theorem requires: a decider is sound, complete, and total. Give up completeness and everything opens up. Rust’s borrow checker rejects some memory-safe programs and is the reason a systems language shipped without use after free. Java’s type checker rejects some programs that would never throw a ClassCastException. mypy, clang-tidy, Infer, and CodeQL all run at scale and find real defects daily. Every one of them answers a three-valued question — yes / no / I reject this rather than guess — while the theorem forbids only the two-valued one. A tool that says “I cannot prove this safe, so I will not accept it” is not defeated by Rice. It is the intended response to Rice.

It does not forbid syntactic properties, and this exemption is larger than it sounds. “Does the source contain eval?”, “is every malloc matched by a free on the same syntactic path?”, “is this identifier ever assigned twice?” — all decidable, all trivially, because they are about the text. A great deal of practical linting is deliberately syntactic for exactly this reason, and the engineering skill is picking a syntactic proxy whose failure modes you can live with. Rice does not apply. It is a theorem about semantics and it says nothing about grep.

It does not forbid deciding the property on a restricted language. Rice quantifies over all Turing-complete programs. Terminating languages (Dhall, Starlark, total fragments of Agda), finite-state models (TLA+ with bounded constants, SPIN), straight-line code, and loop-free circuits all escape completely. SQL without recursive CTEs has decidable equivalence. This is the single most-used escape hatch in practical language design, and it is a design decision, not a compromise.

It does not forbid deciding the property on your program. The theorem forbids a uniform procedure over all programs. seL4 is a verified operating system kernel. CompCert is a verified C compiler. Both are finished, both make absolute semantic guarantees, and neither contradicts anything here, because a proof about one program is not an algorithm for all programs. When someone says verification is impossible because of Rice, they have swapped a quantifier.

It does not apply to intensional properties. “Does this program run in under one second?”, “how many instructions does it execute?”, “how much memory does it allocate?” — these distinguish programs that compute the same function, so they are not semantic in Rice’s sense, and the theorem is silent. (Many are still undecidable, by other arguments. But not by this one, and getting the reason right matters when you need to know whether a restriction will help.)

It does not say the undecidable cases are common in practice. Rice guarantees that some program defeats your analyzer. It says nothing about the density of such programs in real code, and empirically the density is very low — which is why an escape analysis that works on 95% of real Java methods is possible and shipping, notwithstanding that a program exists which defeats it. The theorem describes the worst case, and the worst case is not the workload.

Boundary

Everything that works lives in a well-mapped set of concessions, and it is worth naming them as a set, because a tool is essentially always making one:

• Drop completeness → sound static analysis. Answer {definitely yes, don’t know}, never wrong when it commits. Type systems, abstract interpretation (T047), the borrow checker. The dominant choice where correctness matters.
• Drop soundness → bug finding. Answer {probably yes, probably no}, wrong sometimes, useful anyway. Most linters, signature-based antivirus, heuristic scanners. The dominant choice where coverage matters more than guarantees.
• Drop totality → semi-decision. Answer {yes, still running}. Model checkers, symbolic execution, SMT-backed verifiers. Fine when you can afford to wait and to give up.
• Drop Turing-completeness → decidability returns outright. Total languages, finite-state protocol models, non-recursive query languages. The strongest move available, and the one most often overlooked, because it is made at design time rather than at analysis time.
• Drop “arbitrary program” → per-program proof. seL4, CompCert. Expensive, absolute, and the expense is human rather than algorithmic.

Abstract interpretation (T047) is the principled version of the first concession: it makes “approximate, but only in the safe direction” into a mathematical object with a soundness proof, so that “I gave up completeness” can be stated exactly rather than hoped for. That is the post this one sets up.

Read next