A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
The Rocq Prover was formerly known as the Coq Proof Assistant (see more on the name evolution).
A short introduction to the Rocq Prover
The Rocq Prover is an interactive theorem prover, or proof assistant. This means that it is designed to develop mathematical proofs, and especially to write formal specifications: programs and proofs that programs comply to their specifications. An interesting additional feature of Rocq is that it can automatically extract executable programs from specifications, as either OCaml or Haskell source code.
Fixpoint fac n := match n with | 0 => 1 | S n' => n * fac n' end.n: natfac (S n) = S n * fac nreflexivity. Qed.n: natfac (S n) = S n * fac nn: natfac n > 0n: natfac n > 0fac 0 > 0n: nat
IHn: fac n > 0fac (S n) > 0fac 0 > 0lia.1 > 0n: nat
IHn: fac n > 0fac (S n) > 0lia. Qed.n: nat
IHn: fac n > 0S n * fac n > 0Extraction Language OCaml.