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
“… inspector, in this paper, is a feature of the proof assistant they use — Rocq, which used to be called Coq, and is a cousin of Lean and Isabelle if anyone's heard of those. …”Episode 075 — Growing Code and Proof Together: Verified Systems in Ten Hours Instead of a Year