Coq (Rocq)

Coq, now officially renamed The Rocq Prover, is an interactive theorem prover and proof assistant that has been central to formal verification for over three decades. Based on the Calculus of Inductive Constructions (CIC), Coq allows users to express mathematical definitions, executable algorithms, and theorems, then develop machine-checked proofs of those theorems interactively. It bridges the gap between mathematics and programming, enabling both the formalization of mathematical proofs and the verification of software correctness with mathematical rigor.

History & Origins

The story of Coq begins in 1984 at INRIA-Rocquencourt, where Gérard Huet and Thierry Coquand started implementing the Calculus of Constructions (CoC) in CAML, a functional programming language from the ML family. The theoretical foundation was Coquand’s Calculus of Constructions, first presented in 1985, which provided a powerful type theory capable of expressing both programs and proofs.

Christine Paulin-Mohring joined the project and made a foundational contribution by extending the Calculus of Constructions with primitive inductive types, creating the Calculus of Inductive Constructions (CIC). This extension was critical - it replaced inefficient functional encodings of data types with direct, primitive support, making the system far more practical for real verification work.

Version 4.10, released on May 1, 1989, marked the first mature public release with comprehensive documentation and user guides. In 1991, the system was renamed from CoC to Coq, an indirect reference to Coquand’s name (coq means “rooster” in French), and reflecting the transition to the Calculus of Inductive Constructions.

Over the following decades, the system evolved through major versions. Chetan Murthy restructured the implementation for efficiency in the early 1990s, and Bruno Barras ported the system to Objective Caml (OCaml), which remains the primary implementation language. Hugo Herbelin, Jean-Christophe Filliâtre, and many others contributed significant features, growing the contributor base to over 200 researchers.

The Renaming to Rocq

On October 11, 2023, the development team announced that Coq would be renamed to The Rocq Prover. The new name pays homage to Rocquencourt, the location of the INRIA research center where the project was born. The renaming was completed with the release of Rocq 9.0.0 in March 2025, which marked the official transition. The name “Coq” remains widely recognized and is still commonly used in the community alongside the new name.

Design Philosophy

The Curry-Howard Correspondence

Coq is built on the deep connection between logic and computation known as the Curry-Howard correspondence. In Coq, types correspond to propositions, and programs correspond to proofs. Writing a term of a given type is equivalent to proving the proposition that the type represents. This duality means that Coq serves simultaneously as a programming language and a logical framework.

Constructive Logic

By default, Coq operates in constructive (intuitionistic) logic, where proving that something exists requires constructing a witness. The law of excluded middle and the axiom of choice are not built-in but can be added as axioms when needed. This constructive foundation enables program extraction - automatically generating executable code from proofs.

Trust Through Minimalism

Coq’s architecture centers on a small, trusted kernel that checks proofs. The kernel implements the Calculus of Inductive Constructions and is deliberately kept minimal to reduce the possibility of soundness bugs. Tactics, automation, and user-facing features are built on top of this kernel, but the final proof term is always verified by the kernel itself.

Key Features

Dependent Types

Coq’s type system supports full dependent types, where types can depend on values. This allows encoding precise specifications directly in types:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

(* A vector type indexed by its length *)
Inductive vec (A : Type) : nat -> Type :=
  | vnil : vec A 0
  | vcons : forall n, A -> vec A n -> vec A (S n).

(* A function that only accepts non-empty vectors *)
Definition vhead {A : Type} {n : nat} (v : vec A (S n)) : A :=
  match v with
  | vcons _ _ x _ => x
  end.

Tactics and Proof Automation

Coq provides a rich tactic language (Ltac) for constructing proofs interactively. Rather than writing proof terms directly, users guide the proof through high-level commands:

1
2
3
4
5
6
7

Theorem add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - simpl. rewrite Nat.add_0_r. reflexivity.
  - simpl. rewrite IHn'. rewrite Nat.add_succ_r. reflexivity.
Qed.

Program Extraction

Coq can extract executable programs from constructive proofs in OCaml, Haskell, or Scheme. A proof that “for every input, there exists an output satisfying property P” can be transformed into a function that computes that output, with correctness guaranteed by the proof.

Modules and Typeclasses

Coq supports a module system inspired by ML modules, as well as typeclasses (inspired by Haskell’s) for ad-hoc polymorphism. These features enable large-scale proof engineering and code reuse across formalization projects.

The Vernacular

Coq’s command language, called the Vernacular, provides commands for defining types, functions, and theorems, and for managing the proof environment:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

(* Definitions *)
Definition double (n : nat) : nat := n + n.

(* Inductive types *)
Inductive day : Type :=
  | monday | tuesday | wednesday | thursday
  | friday | saturday | sunday.

(* Theorems *)
Theorem double_injective : forall n m,
  double n = double m -> n = m.

SSReflect

The SSReflect proof language, developed by Georges Gonthier for the four color theorem proof, provides a more concise and compositional tactic style. It has become a standard extension widely used in large formalization efforts.

Evolution

Coq has undergone continuous evolution across its history:

The version 8 series, spanning roughly two decades, brought the most user-facing changes: a complete revision of the concrete syntax for terms, the introduction of the Ltac tactic language, universe polymorphism, and the integration of SSReflect.

File Extensions

• .v - Coq/Rocq source files (Vernacular)
• .vo - Compiled object files
• .vio - Quick compilation files
• .glob - Globalization files for documentation generation

Current Relevance

Coq remains one of the most widely used proof assistants in the world, with an active development community centered at INRIA and collaborating institutions. The system is a cornerstone of formal methods research, used extensively in computer science departments worldwide for both research and teaching.

The ecosystem includes major libraries and frameworks:

• Mathematical Components (MathComp): A library of formalized mathematics built on SSReflect
• Coq Platform: A curated distribution of Coq with commonly used libraries and tools
• opam: Package management through the OCaml ecosystem

Coq continues to be the tool of choice for high-assurance software verification projects, and its influence is visible in newer proof assistants and dependently typed languages that have drawn inspiration from its design.

Why It Matters

Coq’s significance in computing and mathematics is substantial:

1. Pioneering formal verification: Coq demonstrated that formal verification of real-world software is practical, not just theoretical. The CompCert verified C compiler proved that production-quality compilers could be mathematically verified.

2. Resolving mathematical questions: The formal proofs of the four color theorem and the Feit-Thompson theorem showed that proof assistants can handle major mathematical results, providing a level of certainty beyond traditional peer review.

3. Influencing language design: Coq’s dependent type system and proof-relevant programming have directly influenced languages like Agda, Lean, and Idris, shaping how the programming language community thinks about types and verification.

4. Advancing type theory: Decades of Coq development have driven advances in type theory itself, from the Calculus of Inductive Constructions to universe polymorphism and beyond.

5. Education: Through resources like “Software Foundations” by Benjamin Pierce and collaborators, Coq has become a standard teaching tool for programming language theory and formal methods at universities worldwide.