Description #
Coq is a functional programming language and proof assistant used for writing formally verified software and mathematical proofs.
History #
Developed in the 1980s by Thierry Coquand and Gérard Huet, Coq originated from the Calculus of Inductive Constructions. It’s now maintained by INRIA and widely used in academic and industrial settings for software correctness and theorem proving.
Hello World Code #
Definition hello := "Hello, World!".
Eval compute in hello.How to Run #
Option 1: Online
Try Coq Online (CoqIDE)
Option 2: Local
- Install via OPAM or system package manager:
opam install coqOpen CoqIDE or use coqc to compile.
Key Concepts #
- Pure functional language
- Based on constructive logic
- Dependent types
- Formal verification and proof checking
- Tactic-based proof engine
- Type inference
- Pattern matching
- Recursive definitions
- Used in academic and critical systems
- Compatible with OCaml ecosystem
Try It Online #
Fun Facts #
- Coq was used to formally verify the CompCert C compiler, one of the most reliable C compilers ever built.
- Coq’s name is a play on words, referencing both Coquand and the French word for “rooster.”
- Coq proofs can be extracted into OCaml, Haskell, or Scheme code.
