Types that prove a program cannot crash. Church took the untyped λ-calculus and gave it a discipline: annotate every binding, and a checker can decide — before anything runs — that the term will never reach a stuck state. This engine is that checker and its evaluator. Down the center, a term goes in, the type-checker judges it, the small-step evaluator reduces it, and the result comes out. The blue team proves progress & preservation; the red team deletes a check and slips a crash past.
source Church, A Formulation of the Simple Theory of Types (1940), J. Symbolic Logic 5(2):56–68 — jstor.org/stable/2266170 (doi:10.2307/2266170). Rendered, not quoted.
A type is Bool, Nat, or an arrow A→B. Typing is syntax-directed — one rule per shape:
T-Abs λx:A. t : A→B when t:B with x:A. T-App t u : B when t:A→B and u:A (the argument type must match). T-If both branches share one type, guard is Bool. T-Succ/Pred Nat→Nat, T-IsZero Nat→Bool.
Live derivation of the current term (subterm → type; ✗ = untypable):
| subterm | type |
|---|
Church's move is to make safety a theorem you can check mechanically. The typed λ is the-lambda-calculus made safe — the same terms, minus every one that would get stuck.
And the arrow type is a logical implication: a well-typed program is a constructive proof. That is the computational half of the-curry-howard correspondence — types are propositions, programs are their proofs. Each sphere is the next one's premise.
The blue team's live check: re-run the checker & evaluator over every constructed term and confirm progress (no well-typed closed term is stuck) and preservation (type is invariant along the whole reduction), and that every ill-typed term is rejected. If red tampers, this badge is where it shows.
A term is built from a tiny grammar. Values are what evaluation halts on: true, false, a numeral 0, succ 0, …, and an abstraction λx:A. t.
| form | reads | type when |
|---|---|---|
| λx:A. t | a function | t:B ⇒ A→B |
| t u | apply t to u | t:A→B, u:A ⇒ B |
| if c t e | branch | c:Bool, t:T, e:T |
| succ / pred / iszero | arithmetic | Nat→Nat / →Bool |
Every binding carries its type annotation — Church's system is explicitly typed. That annotation is what you feed the panel below.
The checker decides typability from the rules on the spot; the evaluator then reduces the term one small step at a time. Nothing is looked up.
What the machine proves, exhaustively over the constructed terms: every well-typed closed term reduces to a value — never stuck (progress), and its type never changes under reduction (preservation). Every ill-typed term — true true, λx:Bool. x x, succ true — is rejected before it can run. Safety is checked, not hoped.
The blue team's witness (left) re-confirms this live; the red team (right) tries to make it false.
And the checker is conservative: it rejects many programs that would in fact run fine (types are a sound over-approximation, not a decision of "will crash"). To get recursion back you bolt on fix (PCF) — and non-termination returns with it. "Well-typed" is a guarantee about stuck states, nothing more.
"Types make a program correct." Cut. Types prove the absence of stuck states, not that the answer is right — a well-typed sort can still return garbage.
"STLC is Turing-complete." Cut. It is strongly normalizing; every well-typed term halts, so it cannot be.
"Type-checking and type-inference are the same thing." Kept, corrected. This engine checks given annotations; Hindley–Milner infers them. Church's system is explicitly typed.
The red team's move: in T-App, delete the check that the argument's type matches the function's domain. Now (λx:Nat. iszero x) true is admitted — it reduces to iszero true, which no rule steps: a stuck non-value. Progress dies.
Delete the argument-type check and an ill-typed term slips through the checker, then jams in the evaluator. The witness (window 7) recomputes, catches the stuck state, and turns red. Nothing is faked; the attack is real and it is caught.