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.
Table of contents
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
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
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.
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.
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.
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.
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).
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".
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.