MaiaVictor / Formality
- пятница, 19 октября 2018 г. в 00:16:06
Rust
An efficient programming language and proof assistant.
An efficient programming language featuring formal proofs.
Formal proofs: Formality's type system allows it to prove theorems about its own programs.
Optimality: Formality performs beta-reduction (lambda substitution) optimally.
No garbage-collection: Formality doesn't require a garbage collection, making it resource-efficient.
EVM-compatibility: Formality can be compiled to the EVM to run Ethereum smart-contracts.
GPU-compatibility: Formality can also compile to CUDA / OpenCL and run in thousands of cores, making it very fast.
Simplicity: The entire implementation is ~2k LOC and aims to be kept simple.
Theorem proving is possible thanks to dependent functions and inductive datatypes, similarly to Coq, Agda and other proof assistants. To guarantee mathematical meaningfulness, Formality is compiled to Cedille-core, a minimalist type theory which acts as a termination and consistency checker.
Optimality, no garbage-collection, EVM and GPU compatibility are all possible due to compilation to the symmetric interaction calculus, a lightweight computing model that combines good aspects of the Turing Machine and the Lambda Calculus. In order for this to work, Formality enforces some compile-time restrictions based on Elementary Affine Logic.
# Installs formality and enters the `examples` dir
git clone https://github.com/maiavictor/formality
cd formality
cargo install
cd examples
# Evals `add(two, two)`. Output: `Nat.succ(Nat.succ(Nat.succ(Nat.succ(Nat.zero))))`
formality main.for -e four
# Type-checks `add`. Output: `((a : Nat) -> ((b : Nat) -> Nat))`
formality main.for -t add
# Type checks `add-comm`. Output: `((n : Nat) -> ((m : Nat) -> Eq(Nat)(add(n)(m))(add(m)(n))))`
formality main.for -t add-comm
The last example verifies the proof that a + b == b + a
.
Here are some random datatypes and functions to show the syntax, and a proof that a + b == b + a
.
-- Empty, the type with no constructors
data Empty : Type
-- Unit, the type with one constructor
data Unit : Type
| void : Unit
-- Bool, the type with two constructors
data Bool : Type
| true : Bool
| false : Bool
-- Natural numbers
data Nat : Type
| succ : (n : Nat) -> Nat
| zero : Nat
-- Simple pairs
data Pair : (A : Type) -> Type
| new : (A : Type, x : A, y : A) -> Pair(A)
-- Polymorphic lists
data List : (A : type) -> Type
| cons : (A : Type, x : A, xs : List(A)) -> List(A)
| nil : (A : Type) -> List(A)
-- Vectors, i.e., lists with statically known lengths
data Vect : (A : Type, n : Nat) -> Type
| cons : (A : Type, n : Nat, x : A, xs : Vect(A, n)) -> Vect(A, Nat.succ(n))
| nil : (A : Type) -> Vect(A, Nat.zero)
-- Equality type: holds a proof that two values are identical
data Eq : (A : Type, x : A, y : A) -> Type
| refl : (A : Type, x : A) -> Eq(A, x, x)
-- Polymorphic identity function for a type P
let the(P : Type, x : P) =>
x
-- Boolean negation
let not(b : Bool) =>
case b
| true => Bool.false
| false => Bool.true
: Bool
-- Predecessor of a natural number
let pred(a : Nat) =>
case a
| succ(pred) => pred
| zero => Nat.zero
: Nat
-- Double of a number: the keyword `fold` is used for recursion
let double(a : Nat) =>
case a
| succ(pred) => Nat.succ(Nat.succ(fold(pred)))
| zero => Nat.zero
: Nat
-- Addition of natural numbers
let add(a : Nat, b : Nat) =>
(case a
| succ(pred) => (b : Nat) => Nat.succ(fold(pred, b))
| zero => (b : Nat) => b
: () => (a : Nat) -> Nat)(b)
-- First element of a pair
let fst(A : Type, pair : Pair(A)) =>
case pair
| new(A, x, y) => x
: (A) => A
-- Second element of a pair
let snd(A : Type, pair : Pair(A)) =>
case pair
| new(A, x, y) => y
: (A) => A
-- Principle of explosion: from falsehood, everything follows
let EFQ(P : Type, f : Empty) =>
case f : P
-- Returns the first element of a vector which is *statically*
-- asserted to be non-empty, preventing runtime errors.
let head(A : Type, n : Nat, vect : Vect(A, Nat.succ(n))) =>
case vect
| cons(A, n, x, xs) => x
| nil(A) => Unit.void
: (A, n) => case n
| succ(m) => A
| zero => Unit
: Type
-- Returns a vector without its first element
let tail(A : Type, n : Nat, vect : Vect(A, Nat.succ(n))) =>
case vect
| cons(A0, n0, x, xs) => xs
| nil(A) => Vect.nil(A)
: (A, n) => Vect(A, pred(n))
-- The induction principle on natural numbers
-- can be obtained from total pattern-matching
-- This function gets somewhat bloated by type
-- sigs; could be improved with bidirectional?
let induction(n : Nat) =>
case n
| succ(pred) =>
( P : (n : Nat) -> Type
, s : (n : Nat, p : P(n)) -> P(Nat.succ(n))
, z : P(Nat.zero))
=> s(pred, fold(pred, P, s, z))
| zero =>
( P : (n : Nat) -> Type
, s : (n : Nat, p : P(n)) -> P(Nat.succ(n))
, z : P(Nat.zero))
=> z
: () =>
( P : (n : Nat) -> Type
, s : (n : Nat, p : P(n)) -> P(Nat.succ(n))
, z : P(Nat.zero))
-> P(self)
-- The number 2
let two
Nat.succ(Nat.succ(Nat.zero))
-- The number 4
let four
add(two, two)
-- Proof that `2 + 2 == 4`
let two-plus-two-is-four
the(Eq(Nat,add(two,two),four), Eq.refl(Nat,four))
-- Congruence of equality: a proof that `a == b` implies `f(a) == f(b)`
let cong
( A : Type
, B : Type
, a : A
, b : A
, e : Eq(A, a, b)) =>
case e
| refl(A, x) => (f : (x : A) -> B) => Eq.refl(B, f(x))
: (A, a, b) => (f : (x : A) -> B) -> Eq(B, f(a), f(b))
-- Symmetry of equality: a proof that `a == b` implies `b == a`
let sym
( A : Type
, a : A
, b : A
, e : Eq(A, a, b)) =>
case e
| refl(A, x) => Eq.refl(A, x)
: (A, a, b) => Eq(A, b, a)
-- Substitution of equality: if `a == b`, then `a` can be replaced by `b` in a proof `P`
let subst
( A : Type
, x : A
, y : A
, e : Eq(A, x, y)) =>
case e
| refl(A, x) => (P : (x : A) -> Type, px : P(x)) => px
: (A, x, y) => (P : (x : A) -> Type, px : P(x)) -> P(y)
-- Proof that `a + 0 == a`
let add-n-zero(n : Nat) =>
case n
| succ(a) => cong(Nat, Nat, add(a, Nat.zero), a, fold(a), Nat.succ)
| zero => Eq.refl(Nat, Nat.zero)
: Eq(Nat, add(self, Nat.zero), self)
-- Proof that `a + (1 + b) == 1 + (a + b)`
let add-n-succ-m(n : Nat) =>
case n
| succ(n) => (m : Nat) => cong(Nat, Nat, add(n, Nat.succ(m)), Nat.succ(add(n,m)), fold(n,m), Nat.succ)
| zero => (m : Nat) => Eq.refl(Nat, Nat.succ(m))
: () => (m : Nat) -> Eq(Nat, add(self, Nat.succ(m)), Nat.succ(add(self, m)))
-- Proof that `a + b = b + a`
let add-comm(n : Nat) =>
case n
| succ(n) => (m : Nat) =>
subst(Nat, add(m,n), add(n,m), fold(m,n), (x : Nat) => Eq(Nat, Nat.succ(x), add(m, Nat.succ(n))),
sym(Nat, add(m, Nat.succ(n)), Nat.succ(add(m, n)), add-n-succ-m(m, n)))
| zero => (m : Nat) => sym(Nat, add(m, Nat.zero), m, add-n-zero(m))
: () => (m : Nat) -> Eq(Nat, add(self, m), add(m, self))
You can see it on the examples
directory. Soon, I'll explain how to prove cooler things, and write a tutorial on how to make a "DAO" Smart Contract that is provably "unhackable", in the sense its internal balance always matches the sum of its users balances.
Formality syntax (parser / stringifier)
Formality type checker
Formality interpreter
Formality command-line interface
Elementary Affine Logic checks
Cedille compilation (port to Rust?)
Coq compilation
Symmetric Interaction Calculus compilation and decompilation
EVM compilation
Complete CUDA / OpenCL evaluator
IPFS imports
Uncurrying of pretty-printed normal forms
Including dependencies when pretty-printing (so you can copypaste proofs)
Tests
Documentation
This is just a sneak peek. There are missing features and code certainly has bugs. Do not use it use on rocket engines.
See this thread for more info.