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.

Check the official documentation, browse our base-libraries and come hang out with us on Telegram.

Examples

• Adding all numbers of a list:

  sum(xs : List(Number)) : Number
    case xs
    | nil  => 0
    | cons => xs.head .+. sum(xs.tail)

• A proof that negating a bool twice returns the same bool:

  not_not_is_same(b : Bool) : not(not(b)) == b
    case b
    | true  => refl(__)
    | false => refl(__)
    : not(not(b)) == b

• Extracting the first element of a list statically checked to be non-empty:

  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

Usage

Multiple implementations (Haskell, Rust, Go, etc.) will be available in a future. Right now, you can already use the JavaScript one (requires Node v0.12).

Install it via npm with:

$ npm i -g formality-lang

Or via nix, using node2nix, we can also install Formality using the Nix package manager:

$ git clone git@github.com:moonad/Formality.git
$ cd Formality
$ nix-channel --add https://nixos.org/channels/nixpkgs-unstable unstable
$ nix-env -f '<unstable>' -iA nodePackages.node2nix
$ node2nix --nodejs-12
$ sed -i 's/nixpkgs/unstable/g' default.nix
$ nix-env -f default.nix -iA package

It can be used from the terminal with the fm command, or as a library with require("formality-lang").

---

Formality is fully compiled to a 400-LOC Interaction-Net Runtime.