Coq

Coq is an open source programming language created in 1989.

Source code:

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

#168on PLDB

35Years Old

5kRepos

Try now: Web

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...

Coq website
Coq Wikipedia page
Coq is developed on GitHub
Coq docs
There are at least 5,206 Coq repos on GitHub
Coq first developed in The Coq development team
file extensions for Coq include coq and v
Coq on Twitter
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

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.".

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

Coq - Programming language

Language features