Coq - Programming language

Coq is an open source programming language created in 1989 by Thierry Coquand.

#68on PLDB

35Years Old

5kRepos

Download source code:

git clone https://github.com/coq/coq

Homepage · REPL · Source Code · Wikipedia · Subreddit · Twitter · Docs

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Read more on Wikipedia...

Tags: programming language
Coq is developed on GitHub and has 4,738 stars
There are at least 5,206 Coq repos on GitHub
Early development of Coq happened in Inria
Coq is written in Coq, OCaml, Bourne shell, reStructuredText, Markdown, Nix, Python, Tex, CSS, YAML, Make, HTML, C, XML, JavaScript, Bash, Dockerfile, CSV, Lisp, Diff
The Google BigQuery Public Dataset GitHub snapshot shows 793 users using Coq in 1k repos on GitHub
There are 2,066 members in the Coq subreddit
Explore Coq snippets on Rosetta Code
Coq on HOPL
Pygments supports syntax highlighting for Coq
GitHub supports syntax highlighting for Coq
See also: (5 related languages) OCaml, Agda, Idris, C, Isabelle
8 PLDB concepts link to Coq: Coq, F*, hacspec, Ligo, Pygments, Simplicity, UrWeb, V

Example from Linguist:

Require Import FunctionNinjas.All.
Require Import ListString.All.
Require Import Computation.

Import C.Notations.

Definition error (message : LString.t) : C.t :=
  do_call! Command.ShowError message in
  ret.

Definition main : C.t :=
  call! card_is_valid := Command.AskCard in
  if card_is_valid then
    call! pin := Command.AskPIN in
    match pin with
    | None => error @@ LString.s "No PIN given."
    | Some pin =>
      call! pin_is_valid := Command.CheckPIN pin in
      if pin_is_valid then
        call! ask_amount := Command.AskAmount in
        match ask_amount with
        | None => error @@ LString.s "No amount given."
        | Some amount =>
          call! amount_is_valid := Command.CheckAmount amount in
          if amount_is_valid then
            call! card_is_given := Command.GiveCard in
            if card_is_given then
              call! amount_is_given := Command.GiveAmount amount in
              if amount_is_given then
                ret
              else
                error @@ LString.s "Cannot give you the amount. Please contact your bank."
            else
              error @@ LString.s "Cannot give you back the card. Please contact your bank."
          else
            error @@ LString.s "Invalid amount."
        end
      else
        error @@ LString.s "Invalid PIN."
    end
  else
    error @@ LString.s "Invalid card.".

Language features

Feature	Supported	Example	Token
Binary Literals	✓
Integers	✓
Floats	✓
Hexadecimals	✓
Octals	✓
Dependent types	✓	(* http://www-sop.inria.fr/members/Yves.Bertot/tsinghua/tsinghua-1.pdf *)
MultiLine Comments	✓	(* a comment *)	(* *)