Progress and Preservation

Symptom

“Well-typed programs don’t go wrong.” You have heard it. You have probably said it. And then:

String s = null;
s.length();   // NullPointerException

That program is well typed and it went wrong. So either the slogan is false or it means something narrower than it sounds. It means something narrower, and the narrowness is precisely specifiable.

The practical version of the confusion: someone claims a type system prevents bugs, someone else points at a runtime crash in a statically typed language, and the argument goes nowhere because nobody has stated what the guarantee actually is. It is two lemmas. Once you have them, you can say exactly which crashes are excluded and which are not, for any given language, and the answer for Java is different from the answer for Rust and different again for Haskell.

Statement

Type soundness is the conjunction of two properties relating the typing judgement to the operational semantics.

Progress. If $\vdash e : \tau$ then either $e$ is a value, or there exists $e’$ with $e \to e’$.

Preservation (subject reduction). If $\vdash e : \tau$ and $e \to e’$, then $\vdash e’ : \tau$.

Read what each does. Progress says a well-typed term is never stuck now. Preservation says taking a step keeps it well typed, so progress applies again. Neither alone is enough, and their conjunction gives you an invariant that survives arbitrarily many steps.

Milner’s original phrase was “well-typed programs cannot go wrong,” where go wrong had a technical definition: reaching the distinguished error value in his denotational semantics. Everything the slogan lost is in that definition.

Argument

Why both, separately. Consider dropping either.

Without progress, a system could type 1 + true if there is simply no reduction rule for adding a boolean. The term is well typed and stuck. Progress is the lemma that says the typing rules are complete enough: every well-typed non-value has somewhere to go.

Without preservation, a term could start well typed and reduce to garbage. Progress applies only to well-typed terms, so it says nothing after the first step. Preservation is the lemma that says the invariant is maintained, which is what lets you iterate.

Progress is about the present, preservation is about induction over time.

How progress is proved. Induction on the typing derivation. For each rule, show the conclusion is a value or steps. The interesting cases need a canonical forms lemma: if $\vdash v : \tau_1 \to \tau_2$ and $v$ is a value, then $v$ is a lambda abstraction. So in e1 e2, once e1 is a value, it is syntactically a function and the $\beta$ rule applies.

Canonical forms is where the real content sits, and it is the lemma that fails in unsound languages. If null inhabits every reference type, then a value of type String need not be a string literal, so the method-invocation rule has no receiver to dispatch on, and progress fails for exactly that case.

How preservation is proved. Induction on the reduction step. The hard case is $\beta$: show that if $\Gamma, x : \tau_1 \vdash e : \tau_2$ and $\Gamma \vdash v : \tau_1$, then $\Gamma \vdash e[x := v] : \tau_2$. That is the substitution lemma, and it in turn needs weakening and exchange on contexts. Most of the length of a real soundness proof is these structural lemmas.

Java’s null is a documented unsoundness, and it is instructive that it was deliberate. Tony Hoare called it his billion-dollar mistake. The fix is well understood and is what modern languages do: Kotlin’s String? versus String, Swift’s optionals, Rust’s Option<T>, and Haskell’s Maybe all restore canonical forms by making absence a separate type. Progress then holds again, because a value of type String really is a string.

Java’s covariant arrays are the other one, and this one is caught at runtime by design:

Object[] objs = new String[1];
objs[0] = Integer.valueOf(42);   // ArrayStoreException

Both lines typecheck. Preservation fails, because the store rule produces a heap that does not match the static type. Java patches it with a runtime check on every array store, which is a soundness hole closed by paying a cost on every array write forever. C# has the same hole for the same reason, and generics in both languages were later designed with variance annotations to avoid repeating it.

A worked failure trace. Take objs[0] = Integer.valueOf(42) and suppose Java did not insert the check. The static type of objs is Object[], so the store is well typed. After the step, the heap contains an array whose runtime type is String[] holding an Integer. Now String s = ((String[]) something)[0] reads it and hands an Integer to code expecting a String. The term was well typed, took a step, and is now not well typed with respect to the heap. That is preservation failing, and the ArrayStoreException is the runtime enforcing by brute force what the type system did not.

What soundness does not include. Progress says the term steps. It does not say it steps to a value, only that it is not stuck. An infinite loop satisfies progress forever, and is entirely sound. Termination is a separate property (strong normalization) that requires giving up Turing completeness, which is why Coq and Agda have it and Haskell does not (T042).

Forbids

Stuck states in a sound language. No 1 + true, no calling an integer, no reading a field from a function. These are eliminated statically, and the absence of the corresponding runtime check is the performance benefit of static typing.

Preserving soundness with unchecked covariant mutable containers. The combination of subtyping, mutation, and covariance is unsound, and the only options are a runtime check (Java arrays), a variance restriction (C# and Scala generics), or accepting the hole.

Type-based optimization in an unsound language. A compiler that trusts types it cannot rely on generates wrong code. This is why unsafe blocks in Rust are a proof obligation: the compiler optimizes assuming aliasing rules hold, and if your unsafe code violates them the miscompilation is your fault by prior agreement.

Soundness surviving an unrestricted cast. Every escape hatch, from C’s casts to Haskell’s unsafeCoerce, voids the theorem for any program using it.

Does not forbid

It does not forbid runtime errors. This is the misreading behind every “but my typed program still crashed.” Division by zero, array bounds violations, stack overflow, and out-of-memory are all sound: the language defines a step for them, to an exception, so the term is not stuck. Rust panics, Java throws, and Haskell’s head [] errors are all within the theorem, because raising a defined exception is a legitimate transition and not a stuck state.

It does not mean typed languages need no tests. Types prove the propositions that are the types (T042). sort :: [Int] -> [Int] proves the result is a list of integers and says nothing about ordering. QuickCheck and property testing exist for exactly the gap, and the strongest type systems narrow it without closing it.

It does not mean unsound systems are useless. TypeScript is deliberately unsound — bivariant method parameters, any, unchecked index access — and it is one of the most successful type systems ever deployed, because it was designed to type existing JavaScript rather than to prove theorems. Soundness is one design goal traded against others, and the tradeoff can be made correctly in either direction.

It does not require proving it by hand. Soundness proofs are mechanized now: CompCert, the RustBelt project for Rust, and the POPLmark-descended infrastructure in Coq and Agda carry them. RustBelt in particular proved soundness for a realistic Rust subset including the unsafe code in the standard library, which is the interesting part.

It does not say the two lemmas hold only for functional languages. The method is generic. It has been applied to Java, JavaScript, WebAssembly, and Rust. WebAssembly shipped with a mechanized soundness proof as part of its specification, which is the first time a mainstream deployed language did.

Boundary

• Closed terms. The statement is about programs with no free variables. Open terms need the context-indexed version.
• A fixed semantics. Soundness is relative to these reduction rules. Add a feature and you must reprove, which is why language extensions so often introduce holes.
• Sequential. Concurrency needs a different formulation; data-race freedom is a separate theorem, and Rust’s is the notable industrial case.
• No unsafe escape. FFI, reflection, and casts void it locally, and a language’s real guarantee is the theorem plus the size of its escape hatches.
• Says nothing about termination, complexity, or memory use. A sound program can loop forever, allocate unboundedly, and be quadratic where you expected linear.

The precise version of the slogan: well-typed programs do not get stuck, where stuck means no rule applies. Everything a language chooses to define a rule for, including throwing, is not a violation. If you want to know what a type system guarantees, ask which errors it makes stuck and which it makes steps.

Read next