I’m writing this article to talk about the proof and programming language I
developed, Formality, some bits of its history, why it exists and what are its
plans for the future.
Formality is deeply connected to my personal quest, so, to understand its
existence, you must learn who I am. My name is Victor Maia, I’m a 28 years-old software developer and I’ve learned about programming when I was quite young. I immediately felt how much it empowers humans in the times we live and, since then, programming became a hobby and passion through all my life.
The main insight behind self types is easy to explain. Simple functions can be written as
A -> B, and an application
f a has type
B. Dependent functions can be written as
(x: A) -> B x, and an application
f a has type
B a. The insight is that the type returned by an application has access to the value of the argument
a. Self dependent functions can be written as
s(x: A) -> B s x, and an application
f a has type
B f a. The insight is that the type returned by an application can…
Formality is a new programming language featuring theorem proving that, unlike most in the category, is designed to have a familiar syntax and run efficiently. I often associate it with “optimal interaction-net runtimes” that outperform Haskell, Ocaml, Clojure and other functional languages in some very high-order algorithms.
While that is cool, it isn’t mandatory: one of its charms is how it is flexible to different compilation needs. For example, it has a every performant Ethereum backend, where 1 function call uses only 200 gas. Here, I’ll show you how to easily convert its libraries to fast and small CommonJS or…
The initial Ethereum back-end for Formality is deployed on version 0.1.239! That allows you to evaluate high-order, functional programs inside the blockchain. Here, I’ll document this new feature.
Using the new compiler is simple. First, write a Formality program:
| succ(pred : Nat)double(n : Nat) : Nat
| zero => zero
| succ => succ(succ(double(n.pred)))main : Nat
main is a pure function that doubles the natural number 4. Note this is just an example of algebraic datatype manipulation: for actual numbers you’d obviously use native ints instead. To compile this…
Imagine if you could call a function,
f, a googol times. As in, you implement some
f and then repeatedly apply it to a
x, such as
y = f(f(f(f...(x))))), but
10^100 times, and get a result. Seems impossible, right? After all, a googol is so huge that even counting to it would take more years than the lifetime of the universe. In fact, if you could call arbitrary
fs so many times, you could easily break Bitcoin keys! Yet…
Edit: very outdated, access https://github.com/moonad/formality
Formality is a “proofgramming” language aiming to be fast (non garbage-collected, parallelizable, beta-optimal) and simple (with a small specification that can be implemented independently). The type theory behind Formality is called EA-TT. Here, I’ll explain how to install EA-TT and how to port existing Agda code to equivalent proofs on this core.
Since a long time ago, I’ve been looking for a simple theorem prover: a small (say, ~1000 LOC) programming language capable of expressing and proving mathematical theorems about its own programs. If we had such a thing, then developers all around the world would be able to prove assertions about the code they build, and users would be able to trust those assertions without trusting the developers. This quest lead me to many insights and frustrations. I’m writing this post to summarise my journey so far. In the end, I’ll links to potential implementations.
Suppose we write a smart-contract that…
This post is meant to be a summary of my current understanding of this matter, and to present some naive ideas that are probably nonsense.
It has been known for a while that it is impossible to derive induction on the Calculus of Constructions (CoC). That is, there is no term of type:
∀ (P : Nat -> Set) ->
∀ (S : (n : Nat) -> P n -> P (Succ n)) ->
∀ (Z : P Zero) ->
∀ (n : Nat) ->
(I’m using Morte's Church-style syntax because it is familiar.)
Hello /r/ethereum. You may (probably not) remember me from my short talk at Devcon3. There, I presented a working prototype of Moon-Browser. My goal was to build a place where people could not only use Ethereum DApps, but also:
The last one in particular being, I believe, the main benefit decentralization will bring to society. Imagine being able to fork YouTube in a single click. Not just the front-end, not just a video, but…