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.

Eventually I hit…

A proof of function extensionality in Formality

Can we derive function extensionality from self types only?

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…

Cost of a beta-reduction: ~200 gas

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:

T Nat
| zero
| succ(pred : Nat)
double(n : Nat) : Nat
case n
| zero => zero
| succ => succ(succ(double(n.pred)))
main : Nat

Here, 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…

Yes, this is about optimal reductions!

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…

A few years ago, I was experimenting with an “optimal lambda-calculus reduction algorithm”, when I found myself puzzled with the…

Whys, installation, simple types/programs/proofs

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.

1. Installing

At the moment of this writing, EA-TT is implemented in JavaScript. This choice was made because it is the most wide-spread, cross-platform language. Implementing it in other places should take no more than a few days of work. …

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) ->
P n

(I’m using Morte's Church-style syntax because it is familiar.)

In other words, no…

Formal proofs, parallel FVM and ideas for mass adoption

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:

  1. Inspect and modify their codes in a real-time editor;
  2. Verify formal proofs about back-end logic (smart-contracts);
  3. Fork entire apps (including the back-end!) in a single click.

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…

Victor Maia

I’m something that possibly exists

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store