Type Safety and Soundness
In 1985, a rocket-guidance-style question haunted language designers. Can we prove, once and for all, that a well-typed program never crashes? Specifically, can we rule out a "you cannot do that" error at runtime? Not "usually," not "in our test suite" — provably, for every program the type checker accepts. This is the question that Type Safety answers. The answer is delivered by two small, elegant theorems called Progress and Preservation. Together they formalize Robin Milner's famous slogan: "well-typed programs cannot go wrong." The problem this solves is concrete. A type checker inspects a program's syntax before it ever runs. It declares the program "well-typed" if no type mismatches are visible. But syntax-time approval says nothing, by itself, about runtime behavior. Someone must build a bridge between the static world of types and the dynamic world of execution. That bridge is exactly what Progress and Preservation build. They build it one step of computation at a time. This matters far beyond academic curiosity. Many compilers let you skip runtime array-bounds-and-tag checks. Rust, OCaml, and Haskell programmers share an "if it compiles, it probably works" intuition. Every proof-carrying compiler pass in a verified system like CompCert also relies on this. All of these rest on a soundness theorem of exactly this shape. Type safety is a formal contract. It turns a type checker from "a linter that catches typos" into something stronger. It becomes "a machine-checked guarantee about all future executions of your program." This article builds the theorems from scratch on top of the Simply Typed Lambda Calculus. It defines "going wrong" precisely. It states and proves Progress and Preservation. It traces a full worked reduction. Finally, it surveys where real compilers depend on this exact argument. It assumes you already know Static vs Dynamic Typing and the syntax and typing rules of STLC.
- Type safety = Progress + Preservation, proved by structural induction on typing derivations.
- Progress: a well-typed, non-value term can always take a step (it is never "stuck").
- Preservation: if a well-typed term takes a step, the result has the same type.
- Together they guarantee: starting from a well-typed term, every reduction sequence either diverges, reaches a value, or continues stepping — never gets stuck.
- "Stuck" means syntactically valid but semantically meaningless, e.g. applying a number as if it were a function.
- The technique generalizes to almost every statically typed language extension, from references to exceptions to subtyping.
A type system is sound exactly when Progress and Preservation jointly guarantee that no well-typed term ever reaches a stuck state during evaluation.
The idea
A program "goes wrong" in the technical sense used here when it reaches a state that is stuck: it is not a final value, yet no evaluation rule applies to it. The classic example in STLC is applying a boolean as a function, `(true) 3`, or projecting a field that doesn't exist. These are not infinite loops and not values — they are dead ends where the operational semantics has nothing left to say. Crucially, "going wrong" is different from "not terminating." A well-typed program is allowed to loop forever; type safety makes no promise about termination. What it promises is that the program will never wander into semantic nonsense.
Type safety (also called soundness of the type system) is the metatheorem that no well-typed term can ever reach a stuck state, no matter how many evaluation steps are taken. It is proved compositionally through two lemmas that each handle one "half" of the problem:
- Progress: If `⊢ t : T` (the empty context proves `t` has type `T`), then either `t` is a value, or there exists `t'` such that `t → t'`. In words: a well-typed closed term is never stuck right now.
- Preservation (also called Subject Reduction): If `⊢ t : T` and `t → t'`, then `⊢ t' : T`. In words: taking a step never changes — and in particular never destroys — well-typedness or the type itself.
Neither lemma alone gives you safety. Progress alone only tells you the first term in a reduction sequence isn't stuck; it says nothing about the terms produced after stepping. Preservation alone only tells you that if you're well-typed you stay well-typed; it says nothing about whether a well-typed term can actually take a step. It is the induction that chains them together — step, re-apply Progress to the new term (which Preservation guarantees is still well-typed), step again — that produces the full safety guarantee for arbitrarily long executions. This chaining argument is itself a small inductive proof, sometimes stated as a corollary called the Safety Theorem.
How it works
We fix a small operational semantics and type system so the theorems have concrete content, then walk through the mechanics.
Syntax (STLC with booleans, as a canonical running system): ``` t ::= x | λx:T. t | t t | true | false | if t then t else t v ::= λx:T. t | true | false (values) T ::= Bool | T → T ```
Small-step operational semantics (call-by-value): ``` E-App1: t1 → t1' implies t1 t2 → t1' t2 E-App2: v1 value, t2 → t2' implies v1 t2 → v1 t2' E-AppAbs: (λx:T. t) v → [x ↦ v] t E-IfTrue: if true then t2 else t3 → t2 E-IfFalse: if false then t2 else t3 → t3 E-If: t1 → t1' implies if t1 then t2 else t3 → if t1' then t2 else t3 ```
Typing rules (contexts `Γ` map variables to types): ``` T-Var: x:T ∈ Γ implies Γ ⊢ x : T T-Abs: Γ,x:T1 ⊢ t2 : T2 implies Γ ⊢ λx:T1.t2 : T1→T2 T-App: Γ ⊢ t1 : T1→T2, Γ ⊢ t2 : T1 implies Γ ⊢ t1 t2 : T2 T-True: Γ ⊢ true : Bool T-False: Γ ⊢ false : Bool T-If: Γ⊢t1:Bool, Γ⊢t2:T, Γ⊢t3:T implies Γ ⊢ if t1 then t2 else t3 : T ``` The proof of type safety is not a single algorithm you run — it is a mathematical argument you construct once, at the level of the language definition. But it has an algorithmic shape: structural induction over the typing derivation tree, case-splitting on the last rule used. This is exactly how a recursive type checker is implemented, which is why the proof reads like executable pseudocode. ``` PROCEDURE Progress(Γ, t, T) PRECONDITION: Γ is empty, Γ ⊢ t : T (derivation D) POSTCONDITION: t is a value OR ∃ t'. t → t' by induction on the structure of D: CASE T-True, T-False: t is `true` or `false`, already a value. # base case CASE T-Var: impossible: Γ is empty, so x : T ∈ ∅ is false. # vacuous base case CASE T-Abs: t = λx:T1.t2 is a value by definition. # base case CASE T-App: t = t1 t2, Γ⊢t1:T1→T2, Γ⊢t2:T1 by IH on the sub-derivation for t1: EITHER t1 is a value by IH on the sub-derivation for t2: EITHER t2 is a value t1 must be an abstraction λx:T1.t3 # <- uses CANONICAL FORMS so t = (λx:T1.t3) t2 → [x↦t2]t3 via E-AppAbs. DONE. OR t2 → t2' then t1 t2 → t1 t2' via E-App2. DONE. OR t1 → t1' then t1 t2 → t1' t2 via E-App1. DONE. CASE T-If: t = if t1 then t2 else t3, Γ⊢t1:Bool by IH on the sub-derivation for t1: EITHER t1 is a value t1 must be `true` or `false` # <- CANONICAL FORMS again so t → t2 (E-IfTrue) or t → t3 (E-IfFalse). DONE. OR t1 → t1' then t → if t1' then t2 else t3 via E-If. DONE. ``` ``` PROCEDURE Preservation(Γ, t, T, t') PRECONDITION: Γ ⊢ t : T (derivation D), t → t' POSTCONDITION: Γ ⊢ t' : T by induction on D, case-split on the LAST typing rule used simultaneously matched against which evaluation rule fired: CASE T-App with E-AppAbs: t = (λx:T1.t2) v, t' = [x↦v]t2 From T-App: Γ⊢λx:T1.t2 : T1→T2, and by inverting T-Abs, Γ,x:T1⊢t2:T2. From T-App: Γ⊢v:T1. Apply the SUBSTITUTION LEMMA: Γ,x:T1⊢t2:T2 and Γ⊢v:T1 implies Γ⊢[x↦v]t2:T2. So Γ ⊢ t' : T2 = T. DONE. CASE T-App with E-App1 or E-App2: t1 → t1' (or t2 → t2'); apply the IH to the sub-derivation of the part that stepped; typing of t1 t2 is reassembled with T-App using the (unchanged) type of the other part. DONE. CASE T-If with E-IfTrue / E-IfFalse: t' is t2 or t3, both already proved to have type T by T-If. DONE. CASE T-If with E-If: t1 → t1'; apply IH to get Γ⊢t1':Bool; reassemble with T-If. DONE. ``` Two auxiliary lemmas are load-bearing and must be proved before the two theorems above go through:
- Canonical Forms Lemma: if `⊢ v : Bool` then `v` is `true` or `false`; if `⊢ v : T1→T2` then `v` is an abstraction `λx:T1.t`. This is what licenses the "must be" steps in Progress — it rules out a value of function type that isn't a lambda.
- Substitution Lemma: if `Γ,x:T1 ⊢ t : T2` and `Γ ⊢ v : T1`, then `Γ ⊢ [x↦v]t : T2`. This is proved by its own induction on the structure of `t`, and is what makes the `E-AppAbs` case of Preservation work — beta reduction must not break the types.
Complexity & correctness
These are metatheorems, not algorithms, so "complexity" applies to two different things: the size of the proof, and the cost of the type-checking procedure the proof is about. Proof complexity. Progress and Preservation are each proved by structural induction on a single typing derivation, with one case per typing rule (a constant, small number — five to a dozen for realistic core calculi). Each case does O(1) work referencing the induction hypothesis plus, at most, one application of Canonical Forms or Substitution. The Substitution Lemma is itself proved by induction on the term `t`, again one case per syntactic form. So the whole safety proof is finite, mechanical, and — crucially — has been formalized and checked in proof assistants like Coq and Agda for real languages, giving machine-verified confidence rather than "we believe this" confidence. Runtime cost this buys you. This is the real payoff. Because Progress guarantees a well-typed term is never stuck, a compiler is licensed to omit runtime tag checks that a dynamically typed system must perform on every operation. In a dynamically typed interpreter, every application must check "is this actually a closure?" and every arithmetic op must check "are these actually numbers?" — a constant-factor but pervasive O(1)-per-operation tax. A sound static type system moves that check to compile time, done once, so the generated code can dispatch directly. This is precisely why statically typed languages can compile function calls to a direct jump instead of a tag-dispatch, and why array accesses in a soundly typed system with verified bounds (e.g. via dependent types) skip the bounds check entirely. The type checker itself (the algorithm that decides `Γ ⊢ t : T`) is typically linear or near-linear in the size of `t` for simply typed systems — each typing rule inspects a subterm once — though this degrades for systems with subtyping or full inference (see Type Inference and Hindley-Milner for the complications introduced there). Correctness argument, stated cleanly. Define the Safety Theorem: if `⊢ t : T` and `t → t'` (t' reachable in zero or more steps), then either `t'` is a value or `t' → t''` for some `t''`. Proof: induction on the length of the reduction sequence `t → t'`.
- Base case (zero steps): `t' = t`. Apply Progress directly to `⊢ t : T`. Done.
- Inductive case: suppose `t →* t''→ t'` (n steps then one more), and by the inner induction hypothesis `⊢ t'' : T`. Apply Preservation to the step `t''→ t'` to get `⊢ t' : T`. Now apply Progress to `⊢ t' : T`. Done.
This is a clean two-lemma induction: Preservation supplies the well-typedness hypothesis that Progress needs at every single step of an arbitrarily long execution, and Progress supplies the "not stuck" guarantee at each of those steps. Neither could do this alone — Preservation without Progress would only tell you the type is preserved by a stuck term (vacuously true, useless), and Progress without Preservation could not be re-applied after the first step because you would no longer know the new term is well-typed.
Honest tradeoffs. Type safety says nothing about termination — the classic looping term `(λx. x x)(λx. x x)` is ill-typed in STLC (it cannot even be assigned a type, because `x x` would require `x`'s type to equal its own domain, which has no finite solution), so STLC is safe and terminating, but richer systems with recursion (like real languages with `fix` or general recursion) are safe yet can diverge — and that is by design, not a bug in the proof. Type safety also does not imply the absence of all runtime failures: partial functions like division by zero, unsafe array indexing without dependent bounds, or explicit `throw`/`raise` are typically modeled as legitimate final states (or handled with an extended semantics with exceptions) rather than "stuck," precisely so the safety theorem can still be stated and proved for languages that include them. Extending safety proofs to full languages (mutable references, exceptions, subtyping, polymorphism) requires re-proving Canonical Forms and Substitution for the enlarged syntax, and often needs auxiliary machinery like store typings for references — the proof technique generalizes, but the bookkeeping grows.
Worked example
We trace a genuine reduction sequence and show the safety theorem holding at every rung, including one place where the naive reasoning could go wrong if Preservation failed. Consider, in the STLC above, the closed term: ``` t₀ = (λf:Bool→Bool. f (if false then true else false)) (λx:Bool. if x then false else true) ``` First, type it. Let `Γ = ∅`.
| step | derivation fact |
|---|---|
| 1 | `λx:Bool. if x then false else true : Bool→Bool` (by T-Abs, T-If, T-Var, T-False, T-True) |
| 2 | `λf:Bool→Bool. f (if false then true else false) : (Bool→Bool)→Bool` (by T-Abs, T-App, T-If) |
| 3 | applying (2) to (1) via T-App gives `⊢ t₀ : Bool` |
So `T = Bool`. Now we evaluate, checking at each step that Progress applies (the term isn't stuck) and that Preservation holds (the type stays `Bool`).
| n | term `tₙ` | rule fired | type (Preservation check) |
|---|---|---|---|
| 0 | `(λf. f (if false then true else false)) (λx. if x then false else true)` | — | `Bool` ✓ (derived above) |
| 1 | `(λx. if x then false else true) (if false then true else false)` | E-AppAbs, substituting `f ↦ λx....` | `Bool` — T-App reassembles: the substituted body has type `Bool` by the Substitution Lemma applied to step 2's sub-derivation |
| 2 | `(λx. if x then false else true) false` | E-If (inner: `if false then true else false → false`) — congruence into the argument position via E-App2 | `Bool` — argument's type unchanged (`Bool`), so T-App still gives `Bool` |
| 3 | `if false then false else true` | E-AppAbs, substituting `x ↦ false` | `Bool` — Substitution Lemma again |
| 4 | `true` | E-IfFalse | `Bool` — value, Progress terminates the chase here |
At `n = 4` we reach `true`, a value — Progress's "either a value or can step" disjunction resolves on the left branch, and the induction in the Safety Theorem simply stops (there is no requirement to keep stepping). Every intermediate term has type `Bool`, exactly as Preservation guarantees, and every non-value term in the table had an outgoing step, exactly as Progress guarantees. Now the illustrative failure case, to show what the theorems rule out. Suppose someone mistypes the program as: ``` t₀' = (λf:Bool→Bool. f (if false then true else false)) (λx:Bool. x 3) ``` This term is rejected by the type checker at step 2: inside the body `x 3`, we need `x : T1 → T2` for some `T1, T2` by T-App, but `x : Bool` from the lambda's annotation, and `Bool` is not of the form `T1→T2`. There is no typing derivation `⊢ x 3 : anything`, so `⊢ t₀' : T` fails for every `T`. This is exactly the mechanism: the type checker's static rejection is what prevents the term that would eventually reduce to the stuck redex `false 3` from ever being handed to the evaluator in the first place. The theorems don't make ill-typed programs safe — they guarantee that well-typed ones can't reach that stuck shape, and the type checker is the gatekeeper enforcing "well-typed" before execution starts.
Common pitfalls & traps
| Pitfall | Why it happens | Fix |
|---|---|---|
| Proving Preservation without first proving Substitution Lemma | The `E-AppAbs` case silently assumes substitution preserves types; skipping it leaves a hole | Prove Substitution as an independent lemma by induction on term structure, before Preservation |
| Confusing "safe" with "terminating" | Safety only forbids stuck states, not infinite loops | State the theorem's scope precisely: safety ⇏ termination; STLC happens to be terminating for a separate reason (strong normalization) |
| Forgetting Canonical Forms in the Progress proof | Without it, "t1 is a value of function type" doesn't obviously mean "t1 is a lambda" | Prove Canonical Forms as its own tiny lemma from the typing rules for values |
| Treating runtime errors (e.g. division by zero) as automatically "stuck" | Breaks safety proofs for any language with legitimate exceptions | Extend the semantics with an explicit `error` term and prove a three-way Progress: value, steps, or `error` |
| Only checking Progress/Preservation on closed terms, then reasoning about open subterms during the induction | The inductive proof of Preservation must reason about arbitrary contexts `Γ`, not just `∅` | State and prove both lemmas for general `Γ`, and only specialize to `Γ = ∅` in the top-level Safety corollary |
| Extending the language (adding references, exceptions) without re-checking Canonical Forms and Substitution | Adding new value forms can silently break the "must be an abstraction" step | Re-derive Canonical Forms for every new type/value pair introduced |
Pioneers & history
Origins · 1 minRobin Milner and how this was discovered
Robin Milner coined the maxim "well-typed programs cannot go wrong" while developing ML as the meta-language for the LCF theorem prover in the 1970s. His work connected type systems to formal guarantees about program behavior rather than mere syntactic bookkeeping, and it directly motivated the Progress/Preservation proof style formalized by later researchers, most notably Wright and Felleisen. Milner also won the Turing Award in 1991 for his work on LCF, ML, and CCS.
Where this matters
Every soundly typed production language leans on some version of this exact theorem, even when the proof is never published for the full language. The Rust borrow checker's soundness claims (informally, "safe Rust cannot cause data races or use-after-free") are Progress/Preservation-style arguments over an enriched calculus with ownership and lifetimes, and academic formalizations like RustBelt make this precise in Coq. CompCert, a formally verified C compiler, proves semantic preservation across every compilation pass using the same inductive machinery, giving end-to-end guarantees rarely available in ordinary compilers. TypeScript, by contrast, is explicitly unsound by design (it allows certain type-erasing casts and structural gaps for pragmatic reasons), and understanding Progress/Preservation is exactly what lets you articulate precisely where and why TypeScript's guarantees are weaker than Haskell's or OCaml's. Functional language runtimes (OCaml, Haskell, Standard ML, Scala) all rely on soundness to justify eliminating runtime type tags and dynamic dispatch for statically resolved calls, which is a major source of their performance advantage over dynamically typed interpreters for equivalent code. JVM and CLR bytecode verifiers perform a runtime re-check that is itself a Progress-style safety argument, ensuring that even adversarially generated bytecode cannot violate memory safety before it executes. Static analyzers and linters for dynamically typed languages (Python's mypy, JavaScript's Flow) are, in effect, attempts to retrofit a sound type system — and partial soundness, with documented escape hatches, is the central design tension in all of them. Finally, this exact proof pattern is the backbone of every course and paper that formalizes a new language feature: the first thing anyone does when proposing a language extension is ask whether Progress and Preservation still hold, and if not, exactly which case breaks.
Ask the tutor: How would the Progress and Preservation proofs need to change if we added mutable references to STLC?
Does type safety mean my program has no bugs?
No. Type safety only rules out stuck states — situations where an operation is applied to a value it was never designed for, like calling a boolean as a function. It says nothing about logic errors, wrong outputs, infinite loops, or even runtime exceptions that the language explicitly models as legitimate outcomes (like division by zero, if the semantics defines it as raising an error rather than getting stuck). A well-typed program can still compute the wrong answer perfectly safely. Type safety is a floor, not a ceiling: it guarantees the absence of one specific, well-defined category of failure, which happens to be the category that untyped or unsound languages are especially prone to.
Why do we need BOTH Progress and Preservation — couldn't one theorem alone give us safety?
Each theorem only covers "half" of an execution trace. Progress tells you the very first term in a reduction sequence is not stuck, but it doesn't tell you anything about the term produced after one step, because it has no hypothesis relating steps to future well-typedness. Preservation tells you that stepping preserves well-typedness, but a stuck term is trivially not a counterexample to Preservation, since a stuck term never takes a step at all — so Preservation alone can't rule out getting stuck. The full safety theorem is proved by induction on the number of steps, alternating: Preservation supplies well-typedness for the next term, Progress uses that well-typedness to guarantee the next step exists.
Is type safety the same thing as type soundness?
Yes, in standard usage these terms are synonyms, both referring to the metatheorem that well-typed programs cannot reach a stuck state. Some authors reserve "soundness" for the mathematical property of the type system relative to the semantics, and use "safety" more loosely for the resulting engineering guarantee, but in Pierce's Types and Programming Languages and in most modern usage the two are interchangeable. What matters is precisely defining "stuck" for your language and then proving Progress and Preservation relative to that definition — the label attached to the resulting theorem is a matter of house style.
Does every real-world language actually have a proven type safety theorem?
Far fewer than you'd hope, and this is an important honesty check. Fully machine-checked soundness proofs exist for research calculi and for a handful of production-adjacent systems (Rust's core via RustBelt, parts of Java via Featherweight Java, ML dialects). Large, feature-rich languages like C++ or full Python typing extensions typically have no complete soundness proof; their type systems are known or suspected to have soundness holes, sometimes deliberately (for pragmatism) and sometimes as open bugs. TypeScript is explicitly documented as unsound in several specific ways. The theorem is aspirational for most real languages; it is a north star that formal methods researchers work toward, not a universal guarantee you can assume holds.
How does this connect to type inference, like Hindley-Milner?
Type safety and type inference are separate concerns that are often bundled together in practice. Progress and Preservation assume a term is already known to be well-typed — they say nothing about how that typing was discovered. Type Inference and Hindley-Milner is the separate algorithmic question of automatically reconstructing a valid typing derivation (or proving none exists) without explicit annotations, using unification. A language can have a fully sound type system with no inference algorithm (requiring full annotations), or, more commonly, pair a sound type system with a sound and complete inference algorithm, meaning inference finds a typing whenever a valid one exists, and any typing it finds does satisfy Progress and Preservation.
Can a type system be sound but still reject valid, safe programs?
Yes, and this happens constantly — soundness is compatible with, and in fact usually requires, some incompleteness. A sound type system never accepts an unsafe program, but it may reject programs that would actually run safely if executed, simply because the type checker cannot statically prove their safety. The classic example is a well-typed conditional branch that a human can see always takes the "safe" path, but whose safety depends on a runtime condition the type checker can't track. This tradeoff — soundness (no false accepts) versus completeness (no false rejects) — is fundamental and explains why type systems keep evolving (dependent types, refinement types, flow typing) to accept more genuinely-safe programs without sacrificing soundness.
What's the difference between "stuck" and a language's built-in runtime error like an exception?
This distinction is a modeling choice, and getting it wrong is a common source of confusion. If a language treats out-of-range array access as reducing to a designated `error` term via an explicit evaluation rule, then that outcome is a normal, anticipated final state, not a stuck term — the safety theorem is then stated as "reduces to a value, steps further, or reduces to `error`," a three-way Progress. A genuinely stuck term is one the semantics has no rule for at all, like `true 5` in STLC, which represents a case the language designer never intended to occur in well-typed code, and which the type system is specifically built to exclude. Well-designed languages push every anticipated runtime failure into the "modeled outcome" bucket rather than leaving it as an unmodeled stuck state.