An efficient proof language

An efficient proof-gramming language. It aims to be:

  • Fast: no garbage-collection, optimal beta-reduction and a massively parallel GPU compiler make it fast.

  • Safe: a type system capable of proving mathematical theorems about its own programs make it secure.

  • Portable: the full language is implemented in a 400-LOC runtime, making it easily available everywhere.

safe_head(A; xs: List(A), e: length(_ xs) != 0n) : A
  case xs
  + e : length(_ xs) != 0n
  | nil  => absurd(e(refl(__)), _) -- provably unreachable!
  | cons => xs.head
Information updated 07/18/20
View Comments