Rocq (formerly Coq)
The other major interactive theorem prover — the elder peer to lean-theorem-prover in cluster E (formal methods). First released 1989 (developed at INRIA from 1984; original designers Thierry Coquand and Gérard Huet, 200+ contributors since). Renamed from “Coq” to “The Rocq Prover” in March 2025 (v9.0) — the name nods to INRIA Rocquencourt and the mythical bird Roc, keeping the bird theme.
Foundation
Rocq implements the Calculus of Inductive Constructions (CIC) — a dependently typed lambda calculus that doubles as a functional programming language (dependent types) and a higher-order logic (proofs are programs, via Curry–Howard). This is the same family lean-theorem-prover is built on, which is why the two are natural peers: Lean is the younger, more automation/mathlib-and-mainstream-momentum-focused system; Rocq is the older, deeply battle-tested one with a vast verified-software legacy.
Landmark verified developments
- CompCert — an optimizing C compiler largely written and proven correct in Rocq (the flagship “verified systems software” result; rhymes with tla-plus‘s verify-systems goal, but Rocq proves rather than model-checks).
- Four Color Theorem — Gonthier & Werner’s machine-checked proof (2002), which spawned the SSReflect proof-language extension.
- Feit–Thompson (odd-order) theorem — full formal proof completed 2012.
- BB(5) — the fifth Busy Beaver value, proven 2024.
Awarded the 2013 ACM Software System Award.
Why it matters to the wiki
Rocq makes cluster E two-system rather than Lean-only, sharpening the “mechanizing reasoning” lineage (Bush → Leibniz → Hilbert → Gödel → proof assistants): the dream of checking proofs by machine has a 35-year industrial-strength incumbent, not just a rising star. It anchors the proving-math/verifying-software pole that alphaproof (AI-driven proving) now automates and tla-plus (model checking) approaches from the systems side.
Related
lean-theorem-prover · lean-for-programmers · tla-plus · alphaproof · as-we-may-think