coq is an actively used programming language created in 1989. 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 ranks in the top 10% of languages
- the coq wikipedia page
- coq first appeared in 1989
- file extensions for coq include coq and v
- See also: ocaml, agda, idris, mathematical-notation, c, isabelle
- Have a question about coq not answered here? Email me and let me know how I can help.
Example code 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.".
Last updated June 22nd, 2020