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

31Years Old 20Users ?Jobs

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

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
                error @@ LString.s "Cannot give you the amount. Please contact your bank."
              error @@ LString.s "Cannot give you back the card. Please contact your bank."
            error @@ LString.s "Invalid amount."
        error @@ LString.s "Invalid PIN."
    error @@ LString.s "Invalid card.".

Trending Repos

repo stars description

Last updated August 9th, 2020

Edit coq on GitHub