erhannis / formality Goto Github PK

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.

• Bools and some theorems (DeMorgan's laws).

• Monads. (The FP view, not a monoid in the category of endofunctors!)

• A snippet from Data.Vector:

  // A vector is a list with a statically known length
  T Vector {A : Type} (len : Nat)
  | vcons {len : Nat, head : A, tail : Vector(A, len)} (succ(len))
  | vnil                                               (zero)
  
  // (...)
  
  // A type-safe "head" that returns the first element of a non-empty vector
  // - On the `vcons` case, return the vector's head
  // - On the `vnil` case, prove it is unreachable, since `xs.len > 0`
  vhead : {~T : Type, ~n : Nat, xs : Vector(T, succ(n))} -> T
    case/Vector xs
    note e : xs.len is succ(n)
    | vcons => xs.head
    | vnil  => absurd(zero_isnt_succ(~n, ~e), ~T) 
    : T

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 [email protected]: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.