Type Theory and Formal Verification: The Clerk Who Never Gets Tired

Deep End Era. Engineering with Sankalp · Oct 10, 2026 · 57m

Testing a program is different from proving a property about it. This episode starts with types as contracts and the value of making units explicit, then develops the correspondence between proofs and programs. Trusted kernels and proof assistants illustrate how complex arguments are checked against small foundations. Equality, higher structure and AI-assisted proving extend the discussion, while a return to the plant asks where formal methods can make a concrete difference.

Chapters

00:00:00 Cold open: the trip that almost didn't happen

00:03:58 Why testing can't save you

00:08:18 Types as…