Coq

Coq (also known as the Rocq Prover) is a formal proof management system. It provides a formal specification language (Gallina) to define algorithms and state theorems, paired with an interactive environment for writing and checking machine-verified mathematical proofs.

Installation

Install the Coq proof assistant and compiler on Ubuntu:

apt update
apt install -y coq

Optionally, you can install the graphical interface (CoqIDE):

apt install -y coqide

Verification

Verify that the Coq compiler (coqc) is installed:

coqc --version

Writing and Compiling Code

Create a Coq specification file named hello.v:

Require Import Coq.Strings.String.

Module Hello.
  Definition msg : string := "Hello, World!".
End Hello.

Compile the Coq module:

coqc hello.v

Official Resources

• Official Website