Moonad: a Peer-to-Peer Operating System

Victor Maia, John Burnham

Abstract.

We present Moonad, a peer-to-peer operating system. Its machine language, FM-Net, consists of a massively parallel, beta-optimal graph-reduction system based on interaction nets. Moonad's purely functional user-facing language, Formality features a powerful, elegant type-system capable of stating and proving theorems about its own programs through inductive λ-encodings. Online interactions are made through Trellis, a global append-only event-log compatible with both trusted and decentralized backends. On top of those, we build a front-end interface, Moonad, where users can create, deploy and use decentralized applications (Forall), pose and solve mathematical problems (Provit), and exchange scarce virtual assets (Phos).

Table of Contents

• Introduction

• Formality: An efficient functional programming and proof language

• FM-Net: A parallel low-level machine language

• Trellis: A public append-only event-log

• Moonad: An operating system

Introduction

Computing is a field in its infancy. While humans have performed manual computation with fingers, pencil, abacus or quipu since time immemorial, it has been only 75 years since the first general-purpose computing machine was switched on. Given how ubiquitous computers are in our lives today, it can be easy to forget this, but there are hundreds of millions still living who are older than the computer. If a generation in human terms is 25 years, computers users today are at most third-generation.

Accordingly, it should not be surprising that computing systems we use in practice -devices, operating systems, programming languages- lag behind (sometimes far behind) theoretical or experimental systems. Consider that the most popular operating system in the world, Android was designed in the late 2000s, based on a kernel from the 1990s (Linux), which itself was based on a design from the 1970s. There simply hasn't been enough time for all the good ideas to be discovered and to percolate into common use.

For example, most electronic authentication on the web is still done with passwords (sometimes stored in plain-text!), despite the fact that this contributes to tens of billions of dollars lost per year to [identity theft][id-theft] and that secure systems for [authentication based on public key cryptography][pgp] have existed for at least the past 30 years.

In a related area, most electronic commerce is mediated by centralized trusted counterparties, despite the fact that this regularly leads to [data breaches][data-breach] that compromise the security of millions of people. Decentralized systems, such [cryptographic ledgers using byzantine-fault-tolerant chains of signed transactions][bitcoin] and [trustless distributed computing platforms][ethereum] have been under intense development for the better part of the past decade, but have yet to gain widespread adoption.

There has been tremendous theoretical progress in programming language and compiler design, that is barely exploited. We have substructural type systems that can eliminate resource management errors (like segmentation faults) and ensure memory safety. We have proof languages capable of unifying the field of mathematics and programming as one (the Curry-Howard correspondence). In principle, we could have systems software that is formally proven to be error-free, and proof assistants that are both user-friendly enough to be taught in grade-school math class and performant enough to be used on any platform.

Contrast this theoretical progress with our practical record: not long ago, we had a single, small malicious package cause the entire web ecosystem [to collapse][left-pad], [twice][event-stream]. More than 300,000 sites online today are vulnerable to SQL injections. Bugs like heartbleed and [TheDAO][DAO] cause enormous monetary losses. A single [CPU exploit][meltdown-spectre] slowed down nearly every processor in the world by 30%. Faulty software kills people, routinely causing [airplanes to crash][737-max] and hospitals to [stop operating][ohio-hospital].

We believe this mismatch between theory and practice is due to presentation: The technology exists, we need to build the user experience.

Moonad aims to assemble many of these amazing technologies into a decentralized operating system that "just works". We aim to use type theory to build computing systems that are safer, faster and friendlier.

Formality: An efficient functional programming and proof language

The Curry-Howard correspondence states that there is a structural congruence between computer programs and proofs in formal logic. While in theory this implies that software developers and mathematicians are engaged in substantially the same activity, in practice there are many barriers preventing the unification of the two fields. Programming languages with type systems expressive enough to take advantage of Curry-Howard, such as Haskell, Agda and Coq generally have substantial runtime overhead, which makes them challenging to use, particularly at the systems programming level. On the other hand, systems languages such as Rust, Nim or ATS, have shown that type systems can greatly enhance usability and correctness of low-level software, but either have type systems too weak to fully exploit Curry-Howard (Rust, Nim), or introduce syntactic complexity that limits adoption (ATS). In other words, there are lots of slow languages with great type systems and lots of fast languages with lousy type systems.

As programmers and as mathematicians, we don't want to compromise. On one side, mathematicians have the power of rigor: there is nothing more undeniably correct than a mathematical proof. Yet ironically, those proofs are often written, checked and reviewed by humans in an extremely error-prone process. On the other side, programmers have the power of automation: there is nothing more capable of performing a huge set of tasks without making a single mistake than a computer program. Yet, equally ironically, most of those programs are written in an unrigorous, bug-ridden fashion. Formality lies in the intersection between both fields: it is a programming language in which developers are capable of implementing everyday algorithms and data structures, but it is also a proof language, on which mathematicians are capable of proposing and proving theorems.

Formality's types can be seen as a language of specifications that can be mechanically checked by the compiler, allowing you to enforce arbitrary guarantees on your program's behavior. For example, in an untyped language, you could write an algorithm such as:

// Returns the element at index `idx` of an array `arr`
function get_at(i, arr) {
  ... code here ...
}

But this has no guarantees. You could call it with nonsensical arguments such as get_at("foo", 42), and the compiler would do nothing to stop you, leading to (possibly catastrophical) runtime errors. Traditional typed languages improve the situation, allowing you to "enrich" that definition with simple or even polymorphic types, such as:

function get_at<A>(i : Num, arr : Array<A>) : A {
  ... code here ...
}

This has some guarantees. For example, it is impossible to call get_at with a String index, preventing a wide class of runtime errors. But you can still, for example, call get_at with an index out of bounds. In fact, a similar error caused the catastrophic heartbleed vulnerability. Formality types are arbitrarily expressive, allowing you to capture all demands you'd expect from get_at:

get_at*L : {A: Type, i: Fin(L), arr: Vector(A, L)} -> [x: A ~ At(A,L,i,arr,x)]
  ... code here ...

Here, we use a bound, L, to enforce that the index is not larger than the size of the array, and we also demand that the returned element, x: A, is exactly the one at index i. This specification is complete, in the mathematical sense. It is not only impossible to get a runtime error by calling get_at, but it is also impossible to write get_at incorrectly to begin with. Note that this is different from, for example, asserts or bound checking. Here, the compiler statically reasons about the flow or your program, assuring that it can't go wrong with zero runtime costs.

In a similar fashion, you could use types to ensure that the balance of a smart-contract never violates certain invariants, or that an airplane controller won't push its nose down to a crashing position. Of course, you don't need to write types so precise. If your software doesn't demand security, you could go all way down to having fully untyped programs. The point is that the ability of expressing properties so precisely is immensely valuable, especially when developing critical software that demands all the security one can afford.

---

Some readers might object here that while formal proofs can ensure that a program's implementation matches its specification, it cannot eliminate errors inherent to the specification. This is true, but, in many cases, specifications are much smaller than implementations. For example,

spec : Type
  [
    // Demands a List function such that
    sort : List(Word) -> List(Word),

    // It returns the same list in ascendinig order
    And(is_same(xs, sort(ys)), is_ascending(sort(ys)))
  ]

The spec above demands a List function such that it returns the same list in ascending order. Writing and auditing this specification is considerably easier than implementing a complete sort function. As such, formal verification can be seen as an optimization of human auditing: instead of verifying a vast amount of code, you audit a small specification and let the compiler do the rest.

---

An accessible syntax

Proof languages often have complex