01
Coq and the Curry-Howard Path from Proofs to Verified Programs
Coq turned constructive type theory into an interactive proof environment where mathematical proofs become machine-checkable terms and verified programs can be extracted from formal developments.
↗