Formality

A general-purpose programming language for front-end apps, back-end services and smart-contracts. It is:

Fast: no garbage-collection, optimal beta-reduction and a massively parallel GPU compiler make it insanely fast.
Safe: a type system capable of proving mathematical theorems about its own programs make it really secure.
Simple: its entire implementation is ~2k LOC, making it a simple standard you could implement yourself.

Theorem proving is possible due to dependent types, like on other proof assistants. Massively parallel evaluation is possible due to Symmetric Interaction Calculus (SIC), a new model of computation that combines the best aspects of the Turing Machine and the λ-Calculus. No garbage-collection is possible due to linearity: values are simply freed when they go out of scope. To use a variable twice, we just clone it: SIC's lazy copying makes that virtually free. With no ownership system needed, we have Rust-like computational properties with a Haskell-like high-level feel.

Installation
Usage
Examples
Warning

Installation

To install Formality, first make sure you installed Rust:

curl -sSf https://static.rust-lang.org/rustup.sh | sh

Then install it by cloning the repository:

git clone https://github.com/maiavictor/formality
cd formality
cargo install

Usage

Example usage:

git clone https://github.com/maiavictor/formality
cd examples

# Interpreter evaluation
formality everything.formality.hs -e not_true 

# SIC evaluation
formality everything.formality.hs -s -f not_true 

# Type-checking
formality everything.formality.hs -t add
formality everything.formality.hs -t add-comm

Examples

Formality is a very simple language. Its programs are composed of just two building blocks: inductive datatypes, which represent data formats, and functions, which represent computations over those types of data. And that's all you need.

Simple types

One of the simplest types, the boolean, can be declared as:

data Bool : Type
| true    : Bool
| false   : Bool

And the negation function as:

let not(b : Bool) =>
    case b  -> Bool
    | true  => Bool.false
    | false => Bool.true

Pattern-matching is used everytime we want to inspect the value of a datatype.

Recursive types

One of the simplest recursive types, the natural number, can be declared as:

data Nat : Type
| succ   : (n : Nat) -> Nat
| zero   : Nat

And a function that doubles it can be written as:

let double(a : Nat) =>
    case a       -> Nat
    | succ(pred) => Nat.succ(Nat.succ(fold(pred)))
    | zero       => Nat.zero

Since Formality is total, recursion is performed by using the fold keyword, which is available inside cases of a pattern-match. It allows us to recursivelly apply the same logic to structurally smaller values.

Polymorphic types

Types can be easily parameterized:

data Pair<A : Type, B : Type> : Type
| new : (x : A, y : B) -> Pair

Declaring polymorphic functions is as simple as taking types as arguments:

let fst(A : Type, B : Type, pair : Pair<A, B>) =>
    case pair   -> A
    | new(x, y) => x

That allows you to reuse the same implementation of a function for multiple concrete types, a powerful, ancient trick that certain "modern system languages" surprisingly couldn't get right.

Dependent types

Formality allows types to be parameterized not only by other static types, but by runtime values: we call those "indices". The classic Vector type, with a length that is symbolically known at compile time, can be declared as:

data Vect<A : Type> : (n : Nat) -> Type
| cons : (n : Nat, x : A, xs : Vect(n)) -> Vect(Nat.succ(n))
| nil  : Vect(Nat.zero)

When pattern-matching on those, we can specify a return type that depends on indices:

let tail(A : Type, n : Nat, vect : Vect<A>(Nat.succ(n))) =>
    case vect        -> (n) => Vect<A>(pred(n))
    | cons(n, x, xs) => xs
    | nil            => Vect<A>.nil

This allows us to write powerful type-safe functions, such as an indexing function over vectors that can't overflow. We can also use the self keyword to refer to the matched structure itself, allowing us to express mathematical induction (see examples).

Theorem Proving

Those features allow Formality to express theorems as types. For example, mathematical equality can be defined as:

data Eq<A : Type> : (x : A, y : A) -> Type
| refl : (x : A) -> Eq(x, x)

And the proof that a == b implies b == a is just:

let sym(A : Type, a : A, b : A, e : Eq<A>(a, b)) =>
    case e    -> (a, b) => Eq<A>(b, a)
    | refl(x) => Eq<A>.refl(x)

With that much expressivity, Formality types can be seen as a "language of specifications". We can, for example, write "the type of sorted lists", "the type of prime numbers >10", or even "the type of smart contracts that can't be drained".

Optimal Evaluation

The following Formality program:

id(1000000000(List<Bool>, map(Bool, Bool, not), list))

Flips every bit in a list of 100 bits, a billion times. It prints the correct output in 0.03s. You could increase that to beyound the number of stars in the universe, and it'd still output the correct result, instantly. No, your computer isn't doing that many operations: that's possible because Formality is compiled to SIC, an optimal evaluator for functional programs. That allows it to exploit insane runtime optimizations that no other language can, making it often faster than decades-old compilers such as GHC.

More examples

For more of those examples, please check the /examples directory.

Warning

Formality is still at an experimental stage. There are missing features and code probably has bugs. Do not use it use on rocket engines. See this thread for more info.

formality 0.1.10