Coq (software)

Coq is a formal proof management system — a programming language and interactive theorem prover based on the calculus of constructions with inductive types. It implements the Curry-Howard correspondence in its most rigorous form: every program is a proof, every type is a proposition, and the kernel checks every inference. Coq is not a tool for finding proofs; it is a tool for verifying that proofs, once found, are correct. The programmer proposes; the kernel disposes.

Coq has been used to produce some of the most significant formally verified artifacts in computer science. The CompCert C compiler — a realistic optimizing compiler proved correct in Coq — demonstrates that formal verification of industrial-scale software is possible. The Feit-Thompson theorem — a major result in finite group theory whose proof spans hundreds of pages — was formalized in Coq as the Mathematical Components project, settling questions about the proof's completeness that had lingered since the 1960s. The seL4 microkernel, though verified with Isabelle/HOL rather than Coq, belongs to the same tradition: software whose correctness is mechanically proved rather than empirically tested.

Coq's methodology is interactive. The user writes proof scripts — sequences of tactics that transform proof goals — and the system displays the remaining obligations at each step. This is not automated theorem proving in the style of resolution or SMT; it is assisted human reasoning, where the computer checks every step and the human provides the strategy. The cost is time: formal proofs in Coq can take orders of magnitude longer to write than informal proofs. The benefit is certainty: once accepted by the kernel, a proof is guaranteed correct modulo the kernel's own correctness, which has been verified by multiple independent implementations.

Coq represents a radical proposition: that the gap between mathematics and computation is illusory, and that the tools for constructing proofs and the tools for constructing programs are the same tools. The resistance to this proposition is not technical but cultural — mathematicians distrust mechanized proof, programmers distrust formal methods, and both communities are slower to adopt verification than the stakes of their errors would justify. Coq is not the future of computing. It is a demonstration that the future has been possible for decades, and that our delay in reaching it is a choice, not a constraint.