Definition
Plain language
A programming language for writing mathematical proofs that a computer checks line by line.
As stated in the literature
An interactive dependently-typed proof assistant (since renamed Rocq) with a small trusted kernel that mechanically verifies each proof step; the verification substrate behind verified-systems work like CompCert and seL4.
Why it matters: It provides machine-checked certainty for proofs and critical software, so you can trust that something is correct rather than just hoping a human reviewer didn't miss a flaw.
For example, a mathematician can write out a proof in Coq and the computer will refuse to accept it unless every single step truly follows from the last.
Heard on the show
“Systems like Coq and Lean, where you write the proof in a language so precise that a machine can check it.”Episode 122 — When Your Coding Agent Lies About the Fix: Verifying the Plan Before the Model Runs