Thoughts about Formality

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.

A personal quest for perfection

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 plateau and started obsessing about programming languages, looking for one that made me faster and more productive. I learned every language I could. C, C++, Java, C#, JavaScript, PHP, Python, Ruby, Lua. Each one was beautiful in its own way, but none satisfied the hunger deep inside my soul, so I went deeper: APL, J, SmallTalk, and, finally, Lisp, which, after reading Beating the Averages, seemed like the ultimate answer for a while. Eventually, I concluded macros aren’t so special and that Lisp lacked something very important: types. This led me to Ocaml, Elm, PureScript, our beloved Haskell and, finally, Agda and Idris.

From Agda and Idris to Formality

Five years later and I still consider those two languages the closest
to perfection that we have. They are beautiful and amazing in so many senses. Regardless, they still have flaws, of which two stand out. The first one is efficiency: neither of those had a viable compiler. Nowadays, the situation improved a lot, but they are still inherently slower than, say, C, in very fundamental ways, which goes against the notion of perfection. The second flaw was complexity: in my mind, a perfect language would be simple and elegant, just like the most beautiful equations, but both Idris and Agda are big, monolithic, human-engineered projects, with normal bugs and flaws.

In an attempt to make an Agda/Idris that was efficient and elegant, I started developing Formality. After years of constant learning and improvements, the language is now actually quite good, and I’m very proud of it. In some senses, it is objectively better than others. Our JavaScript output is very good, our syntax is much terser in some cases, we have an interaction net runtime that can be used to explore optimal reductions, our type-checker is by far the fastest, it can perform optimizations that are simply impossible in any other functional language, and our trusted core is a 500-LOC file, making it arguably the smallest, most elegant proof language around.

For illustration, here is the compilation of List.map to JavaScript:

// Maps a function over a list (in Formality).
List.map<A: Type, B: Type>(f: A -> B, xs: List(A)): List(B)
  case xs:
  | List.nil<>;
  | List.cons<>(f(xs.head), List.map<,>(f, xs.tail));
// The generated JavaScript output.
var List$map = f => as => {
  var self = as;
  switch (self._) {
    case 'List.nil':
      return List$nil;
    case 'List.cons':
      var $2 = self.head;
      var $3 = self.tail;
      return List$cons(f($2))(List$map(f)($3));
  }
};

And here is the Black Friday Theorem (half of the double is the same):

// A natural number (non-negative integer)
T Nat
| zero;
| succ(pred: Nat);
// Double of a natural number
double(n: Nat): Nat
  case n:
  | zero;
  | succ(succ(double(n.pred)));
// Half of a natural number
half(n: Nat): Nat
  case n:
  | zero;
  | case n.pred:
    | zero;
    | succ(half(n.pred.pred));;
// Black Friday Theorem: half of double is the same
bft(n: Nat): half(double(n)) == n
  case n:
  | Equal.to<_,zero>;
  | Equal.apply<_,_,_,_,Nat.succ>(bft(n.pred));
  : half(double(n.self)) == n.self;

(To try it, install Formality with npm i -g formality-lang, save the file as .fm (exactly that name) and run fm to type-check, or fmjs <term_name> to compile.)

5 steps to perfection

Sadly — and this is very hard to admit — even after so much effort and work, Formality is still way too far from perfection in so many areas. In my opinion, there are 5 major issues that demand large improvements:

1. The user-facing syntax still needs a lot of work to feel powerful.
2. We must get rid of JavaScript and write the language in itself.
3. The interaction-net runtime still needs research.
4. We need a termination checker and consistency proof.
5. We need to incorporate important insights from HoTT.

Each item in this list is a big, independent problem that requires significant effort. For example, for the language to be really productive, we need an Agda-like dependent pattern-matching notation, better unification, better imports, better implicits, better goal displaying and, who knows, some GPT-3-like program synthesis using types instead of English as the spec? Making the interaction net runtime viable still depends on open research problems like reduction soundness (EA-Linearity? LambdaScope?) and practical efficiency (GPU runtime?). HoTT’s treatment of equality is just too good to pass, but implementing it (specially transp) is complex. And so on.

If I magically had a solution for all those problems overnight, I’d be posting everywhere about how Formality is the most perfect language in the world, but the reality is still far from that. In its current state, Idris and Agda are objectively better in several aspects.

What is next?

I’m personally tired. Idris 2 is turning out very good, sometimes I wonder if I should just help with it, but it still lacks important features we have, and it seems to suffer similar problems (there is just too much to be done for it to be great). I wish I had more time to implement features, to learn about HoTT, to research interaction nets and better unification algorithms. There is just so much to do, so much to learn, and so little time to live.

For now, I really need a break from hard subjects. My plan is to spend the next weeks just making some silly games in the language I built, improve its ecosystem and fix any issues I encounter. I’ve just started scratching the concept of Moonad, a decentralized operating system entirely built on top of a proof language instead of C (check http://moonad.org/play/Mons to preview a Pokémon-like game I’m developing on it) and I really like that concept.

Eventually, though, I admit I must sit down and think about the motivations and feasibility of my goals. There is only so much a few devs can do alone, and I need to consider that when structuring my plans. I admit sometimes I do wish we had just a fraction of the resources some suspicious crypto projects raise; it is currently very hard to fund a research project like Formality that doesn’t have a clear short-term commercial value. But that’s ok, it is how the market work and that is nothing wrong with that. I’ll keep doing my best to push my ideas forward, and, faster or slower, I hope I can eventually change the world with my efforts!