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`

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 The Coq development team
- 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.".
```

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 *) | (* *) |