Lesson 264
Dependent Types & Proof Assistants
dependent types · Curry-Howard · Coq/Lean/Agda
1:00How types that encode values turn programs into machine-checked proofs, and why that enables verified compilers, kernels, and theorems.
By the end, you can
- Explain what distinguishes a dependent type from ordinary generics, using Vec Int 3 as the example.
- Describe how the type of `append` encodes a length law and why the type-checker enforces it at compile time.
- Explain why `head` on a length-0 vector is a compile-time type error, not a runtime crash.
- State the Curry-Howard correspondence and map proposition, proof, implication, and conjunction to their programming counterparts.
- Trace the three-stage pipeline of a proof assistant: tactics, proof term, kernel.
- Justify why the trusted kernel is kept small, and why functions in types must be total.
- Identify CompCert, seL4, the Four-Color Theorem, and Feit-Thompson as major verified landmarks and explain what was verified in each case.
Up next in Advanced Algorithms, Math & PL Theory
