What Undecidability Costs Real Tools

Line up what the tooling on a normal project is trying to establish. Will this array index go out of bounds? Can this pointer be null here? Is this lock always released? Does this refactoring preserve behaviour? Does this loop terminate?

Every one of those is a semantic property of the program, and every one is non-trivial, so Rice's theorem says no algorithm decides any of them.

And yet the tools ship, run in continuous integration, and catch real defects. There is no loophole involved. What they abandon is the requirement that made the question impossible: answering correctly on every program. Drop either half and the space of achievable tools opens up immediately.

The engineering question is therefore not whether to be wrong. It is which kind of wrong to be, and that choice is the single most important fact about any analysis tool.

Fix a property, say "this program never dereferences null". An analyser reports either safe or warning. Two error modes exist and they cannot both be eliminated.

A false alarm is a warning on code that is actually fine. A missed bug is a clean report on code that is actually broken.

An analyser is called sound for the property when it has no missed bugs: if it says safe, the code is safe. The cost is false alarms, and the cost is not optional. It is the undecidability, paid in a currency the tool can survive.

An analyser that instead eliminates false alarms will miss bugs. Silence from it means nothing was found, not that nothing is there.

Both are legitimate. They serve different jobs, and confusing them is how teams end up trusting a tool for a guarantee it never claimed.

Three exits from the same impossibility, and a tool takes exactly one.

The first two keep the language as it is and give up on one error mode. They are duals, and the trade is quantitative: pushing false alarms down on a sound analyser means weakening its abstraction until it starts missing things.

The third exit is different in kind. Rather than approximating the answer, it removes the programs that make the question hard. If a language cannot express unbounded recursion, termination is decidable for it outright, and no approximation is needed.

The choice is visible in every tool's documentation if you know to look for it, and it is usually stated as what the tool guarantees rather than as which error it tolerates.

The sound branch is not a theoretical position. Astree is a static analyser for C built on abstract interpretation, and it is designed to prove the absence of runtime errors: overflow, division by zero, out-of-bounds access, and similar.

It is sound, so a clean report is a proof rather than an absence of evidence. It was applied to the primary flight control software of the Airbus A340 and later the A380, and on that target it reached the outcome that makes sound analysis practical rather than merely correct: zero false alarms.

That number deserves attention, because a sound analyser is entitled to produce false alarms and usually does. Reaching none is not a consequence of soundness. It comes from tuning the abstract domains to the specific shape of the code being analysed, which is feasible for control software generated from synchronous specifications and much harder for arbitrary C.

It is tempting to read every imprecise answer as an implementation shortcut. For pointers there is a theorem saying otherwise.

William Landi established the result in "Undecidability of Static Analysis", ACM Letters on Programming Languages and Systems, volume 1, issue 4, 1992, pages 323 to 337. In a language with conditionals, loops, dynamic allocation and recursive data structures, precise alias information cannot be computed. The may-alias relation is not recursive, and the must-alias relation is not even recursively enumerable.

G. Ramalingam sharpened and extended the treatment in "The Undecidability of Aliasing", ACM Transactions on Programming Languages and Systems, volume 16, issue 5, 1994, pages 1467 to 1471.

Read the two relations against the tiers from the previous lesson. Must-alias sits in the bottom tier, so it cannot even be confirmed by unbounded search. Any tool reporting that two pointers definitely alias is reporting a sufficient condition, never the exact answer.

Undecidability shows up in ordinary review comments. Consider a checker deciding whether the indexing below is in bounds.

def pick(xs, flag):
    i = 0
    while collatz_step(i) != 1:    # halts? nobody knows in general
        i += 1
    return xs[i] if flag else xs[0]

To prove xs[i] safe the checker must bound i, which means knowing when that loop exits, which is the halting problem. A sound checker therefore warns, even if a human can see the loop is fine for the inputs that actually occur.

This is the everyday texture of the theory. The warning is not a bug in the tool and no amount of engineering removes it. It is why sound analysers offer annotations, assumptions and suppression: those are channels for a human to supply the fact the tool provably cannot derive.

The undecidability results all assume the language can express arbitrary computation. Remove that and they stop applying.

Proof assistants take this exit deliberately. In Coq, Agda and Lean, every function must be shown to terminate, usually by structural recursion on an argument that provably shrinks. The resulting language is total: it cannot express a non-terminating program, so termination is trivially decided, and the cost is that some genuinely terminating algorithms must be restructured or proved terminating by hand before they are accepted.

The same bargain appears far outside verification, usually without being named. Regular expressions are not Turing complete, which is exactly why matching can be linear-time. A configuration format that cannot loop is a format whose evaluation always terminates.

Every one of these is the same trade: expressive power surrendered in exchange for a guarantee that is unobtainable above the line.

The fourth column is the one to read first, because it is what the tool actually licenses you to believe.

Most production setups combine rows rather than picking one, and the combination is coherent precisely because the rows fail differently. A bug finder and a test suite both stay silent for reasons that are not evidence of correctness. A sound verifier's silence is evidence, and it is bought with alarms elsewhere.

The arc of this cursus is one narrowing question. Finite states could not count. A stack could count one thing at a time. A tape removed the memory limit entirely, and what remained was not a shortage of resources but a genuine impossibility, provable in eight lines and generalised by Rice to every semantic property at once.

The practical yield is not pessimism. It is that a whole family of proposals can be dismissed without investigation. A tool that promises exact answers to a semantic question about arbitrary programs is either restricting the language, approximating in one direction, or mistaken, and knowing which takes one question rather than a pilot project.

The theory does not say what cannot be built. It says precisely what any build must give up, and that turns an open-ended engineering argument into a choice with three named options.