Real World: Type Systems & Functions

Math for CS · Axiom Academy

REAL WORLD Type Systems & Functions How formal language theory became the backbone of modern programming languages 1. The Bug That Costs Billions Most production bugs are not algorithmic mysteries. They're category errors — treating dollars as cents, miles as kilometers, an unauthenticated user object as an authenticated one, an empty optional as if it were filled. A surprisingly large slice of all software bugs comes down to "this thing wasn't the kind of thing I thought it was." A type system is a formal language that lets the compiler refuse to ship code where one kind of thing flows into a slot expecting another kind. It's a static, mathematical filter sitting in front of your runtime. And underneath that filter is a single piece of math: the simply typed lambda calculus , invented by Alonzo Church in 1940 — six years before the first stored-program computer. 2. The Lambda Calculus in 90 Seconds Lambda calculus is the smallest possible programming language. There are only three things you can build: Functions (abstractions): x.\,M — "the function that takes x and returns M " Application: M\,N — "apply function M to argument N " The only computation rule is beta reduction : substitute the argument for the bound variable.

This is the written version of the interactive lesson above. See the full Math for CS course.