Top 1,000 Features Creators Resources Extensions Blog Explorer CSV Download
GitHub icon


< >

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

#64on PLDB 35Years Old 5kRepos
Download source code:
git clone

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

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 Token Example
Binary Literals โœ“
Integers โœ“
Floats โœ“
Hexadecimals โœ“
Octals โœ“
Dependent types โœ“
(* *)
MultiLine Comments โœ“ (* *)
(* a comment *)

View source

- Build the next great programming language ยท About ยท Acknowledgements ยท Published by Breck's Lab