Type Safety and Soundness

Every time a compiler rejects "hello" + true or a call with the wrong number of arguments, it has just proved a little theorem about your program — before it ever runs. That is the quiet magic of a type system: it is a lightweight, automatic correctness proof, run on every program, that rules out a whole class of disasters. Robin Milner distilled the promise into a slogan in 1978: "well-typed programs don't go wrong."

This page is about what that slogan means precisely, and how you actually prove it. "Go wrong" isn't a mood — it is a formal notion of a stuck, nonsensical state. And the guarantee that well-typed programs never reach one is a genuine theorem, type soundness, with a two-part structure that has been the template for language design ever since. It sits atop ordinary type systems and the operational semantics that give a language meaning.

What "go wrong" means: operational semantics

To prove programs don't go wrong we must first say, exactly, how they run and what "wrong" is. A small-step operational semantics defines a relation e \longrightarrow e' — "term e takes one step of computation to e'." Evaluation is a chain e \longrightarrow e_1 \longrightarrow e_2 \longrightarrow \cdots, and there are exactly three fates for a term:

It reaches a value — a finished result like 5 or \texttt{true} or a \lambda-abstraction. Good.
It steps forever — diverges. Not "wrong", just non-terminating.
It gets stuck: a non-value with no applicable step, like \texttt{true} + 3 or 3(\texttt{true}) (applying a number as if it were a function). This is "going wrong."

A stuck state is the formal ghost of a segfault, a NoMethodError, or the C-style undefined behaviour where a bit pattern is used as the wrong kind of thing. Type safety is precisely the promise that a well-typed term never lands in the third case.

The soundness theorem = Progress + Preservation

Write \vdash e : \tau for "e is well-typed with type \tau." Type soundness is the theorem that such an e never gets stuck. It is proved as the conjunction of two lemmas — the great one-two punch, due to Wright and Felleisen (1994):

Progress: if \vdash e : \tau, then either e is a value, or there exists e' with e \longrightarrow e'. A well-typed term is never stuck — it can always make progress.
Preservation (a.k.a. subject reduction): if \vdash e : \tau and e \longrightarrow e', then \vdash e' : \tau. Taking a step preserves the type.

Now chain them. Start well-typed. By Preservation, every step keeps you well-typed. By Progress, at every well-typed point you are either done (a value) or can step again. So you can never reach a stuck non-value: the two lemmas interlock into an induction over the whole evaluation sequence. That is the entire proof of "well-typed programs don't go wrong" — a simple induction once the two lemmas are in hand.

A glimpse of the rules

Both lemmas are proved by induction on the structure of typing derivations, using inference rules of the same shape you met in Hoare logic — premises above the line, conclusion below. Two typical rules for a tiny functional language: how to type a function, and one step of computation.

\dfrac{\Gamma, x{:}\tau_1 \;\vdash\; e : \tau_2}{\Gamma \;\vdash\; \lambda x{:}\tau_1.\,e \;:\; \tau_1 \to \tau_2} \qquad\qquad (\lambda x{:}\tau.\,e)\; v \;\longrightarrow\; e[x := v]

The left rule says a lambda has an arrow type when its body has the result type assuming the parameter's type (the context \Gamma carries those assumptions). The right rule is beta reduction: applying a function to a value substitutes the value for the parameter. Preservation for this step is the crux — it needs a substitution lemma (substituting a value of the right type preserves typing), which is where most of the real work of a soundness proof lives.

// The slogan in miniature. TypeScript rejects each stuck term before it runs: const n: number = 3; // n(true); // ✗ type error: "this expression is not callable" // const s: string = n; // ✗ type error: number is not assignable to string const ok: number = n + 1; // ✓ well-typed: steps to the value 4, stays a number // Progress: a well-typed term is a value or can take a step (never stuck). // Preservation: n + 1 : number, and after it computes, 4 : number — type preserved.

Yes — and this is the deep idea. A typing derivation \vdash e : \tau is a finite tree of inference rules: a bona fide formal proof, checked mechanically by the compiler, that e enjoys the property "never gets stuck." It is a lightweight proof because the property is fixed and modest (no divide-by-zero, no calling a non-function) and the checking is fully automatic — no human writes invariants. That trade — a weaker guarantee than full functional correctness, but free and universal — is why type systems are the most widely deployed formal method on Earth by orders of magnitude. And the Curry–Howard correspondence reveals it is no analogy at all: types are propositions and programs are their proofs.

When soundness fails: real-world holes

A type system that admits a stuck state is unsound — its "proof" has a bug, and a well-typed program can still go wrong. Two famous holes in mainstream languages:

Java's covariant arrays. Java lets \texttt{String[]} be used where \texttt{Object[]} is expected (arrays are covariant). So Object[] a = new String[1]; a[0] = 42; type-checks — but storing an Integer into a String array must fail. Java patches the hole with a runtime ArrayStoreException: the static type system alone is unsound here, and a dynamic check papers over it.
Null. In languages where null inhabits every reference type, a well-typed String s = null; s.length(); passes the type checker yet crashes — Tony Hoare's self-described "billion-dollar mistake." The type says "a String", the value is nothing, and the method dispatch goes wrong. Modern languages close this with non-nullable types and explicit Option/? types.

Both are Preservation failures in spirit: a step (an array store, a method dispatch) lands in a state the static type promised couldn't happen. Studying them is the best way to feel why soundness is a theorem to be proved, not a property to be assumed — every escape hatch (a cast, covariance, null, C's unchecked unions) is a hole an adversary can drive a stuck state through.

Soundness is a modest promise, and over-reading it is the classic mistake. It guarantees your program won't reach a stuck state — no adding a boolean to a function, no calling a number. It says nothing about whether your program computes the right answer: a perfectly well-typed function add(a: number, b: number) { return a - b; } is type-safe and utterly wrong. "Doesn't go wrong" means "doesn't get stuck", a specific technical fate — not "is bug-free". Nor does it forbid non-termination or logic errors or exceptions the language chooses to define. The type checker proves one small theorem for free; proving your program does what you meant is the job of the heavier machinery — contracts, Hoare logic, and verification — elsewhere in this course.