Click here for a Russian translation of this post (opens new window) made by remimimimi (opens new window)

Over the last roughly two years I've been on a slow and frustrating journey. After learning Rust a few years ago and beginning to seriously use Typescript, I've become progressively obsessed with typesafety, and extremely impatient dealing with code that has easily preventable bugs and errors. Especially in my work (opens new window), in which I've been forced to use python to build large-scale data pipelines, I become extremely irate when a pipeline crashes after running for hours because of environment-specific mistakes that could have been found in seconds using a typechecker.

I've been trying my best to make everything I work on typesafe and harassing people around the internet (opens new window) to do the same. It is this obsession that has driven me on the painful path I'll describe in this post, where I vainly build project after project to try to close serious gaps in my toolchain's soundness, only to realize that those gaps can't truly be closed without going deeper down the stack and solving even more difficult problems. This journey downward has made me absolutely convinced it's inevitable and imperative that the software engineering discipline fully embrace formal verification (opens new window), the academic niche that studies how to guarantee not just basic type soundness, but overall correctness using logical proofs. We can't keep building our society on top of a quicksand software infrastructure.

After two years of learning as much as I can about formal verification and proof assistants like Coq (opens new window), I finally feel I know enough to be brave and push forward with an idea that's felt urgent for a long time: I'm now hell-bent on building a new programming language intended to bring formal verification and provably correct software to the engineering mainstream. I'm calling this language Magmide, and I invite you to check out the repository to understand the project in more detail (opens new window).

However in this post I want to share the history of my journey, to help both myself and others understand what I've been up to, how I've ended up where I am, and what lessons I've learned. Some lessons I feel I've learned:

• Get feedback earlier! Don't be so precious and afraid about putting your ideas into the world.
• Pursue your best idea first. Don't waste time on things that just seem "practical" but aren't actually that convincing. It's better to iterate toward your best idea or approach it at an angle than to hide behind ideas that aren't actually exciting.
• Ask for help! We achieve the best things when we find the others and work together. Doing something all by yourself isn't going to impress people as much as you think.

The best way to share my path is to look at all the major personal projects I've worked on. I've looked at their git commit histories to guess a fuzzy timeline of when each project was receiving substantial work. Some of the projects directly inspired others or had significant overlap, so the date ranges also overlap at many times.

thin-ql (opens new window): 2019-02-09 to 2020-02-12

I'm extremely annoyed at the object-relational impedance mismatch (opens new window). For years I've longed to find a database that had strong ACID-like consistency guarantees, great performance, strongly-typed schemas and data integrity capabilities, and an object-graph query interface. However nothing really is sufficiently better than postgres to justify the trouble, so the best I've been able to find are projects that just provide an object-graph translation layer on top of postgres, such as postgrest (opens new window) and postgraphile (opens new window). These projects are both great, and they're mostly good enough for me to be excited about using them at work. Postgraphile especially seems to be a great fit for a practical web app, especially when combined with graphql typescript generators (opens new window).

However when I discovered these tools they weren't as mature, and they both a couple big problems I wasn't willing to look past for many projects: they both expose a fully dynamic api to all outside consumers instead of a narrow whitelisted api; and they weren't rigorously typesafe all the way down. What I really wanted was to take a known list of graphql-like queries, metaprogrammatically generate server code that only served those queries, and make the whole thing statically typed at every layer. I had been wanting to play around with asynchronous Rust, so I got to work. I pursued it off and on for a while.

I actually got this project working for many query types! However at some point I realized that postgres itself wasn't really as typesafe as it should be, since it suffers from the billion dollar mistake (opens new window) of allowing every value to be potentially null. In the Magmide repo (opens new window) I discuss some of the possibilities for things Magmide could build, including a multi-persistence metaprogrammatic database that I intend to pursue after Magmide is working.

ts-std (opens new window): 2019-07-04 to 2020-02-26

The previous project thin-ql was the first I had seriously pursued in Typescript, so I found myself often missing various abstractions in Typescript, such as handy utility types and Result-style monad types. As I was working on thin-ql I put common abstractions into this library, adding things to it as they came to me. I eventually moved this repo into my employer's organization, since we began to use it heavily in work projects.

kreia (opens new window): 2019-09-27 to 2020-02-16

Almost all of these major projects have some custom domain specific language at their heart, which means they needed a parser. I had looked all around for a parser generator or other parsing tools that were both well-designed and typesafe-first, but couldn't find anything I liked. So I built my own!

This period of time is actually only the most recent push on this project, when I refactored it out of the untyped javascript I had originally built it in. This version even defines its own domain specific language to define language grammars, and from those grammars a compiler creates a typescript parser scaffold that a project can fill in with custom logic. I got it working enough to use in these other projects, although there are many rough edges and tricky cases. I intend to revisit these concepts once Magmide is working (and likely even before in order to get Magmide working!), since parsing is such a well-defined logical problem and can massively benefit from verification.

coq-playground (opens new window): 2020-01-22 to 2020-04-05

Around this time I got interested in actually learning Coq, and started reading Software Foundations (opens new window). But at this point I was terrified of the language and didn't really believe I could use it to achieve anything concrete. I went through many of the exercises and was fascinated by the tool, but I was too scared to think I should really invest serious time in it.

Although this date range was when I was seriously working through exercises, I kept finding as many resources as I could, reading and playing around, and continually being pulled back to formal verification as a concept. Even though I kept trying to force myself to work on something "practical", this obsession would bubble under the surface from this point on.

project-f (opens new window): 2020-03-10 to 2020-07-27

As I alluded to earlier, I had become extremely annoyed with the general lack of typesafety in the Vue frontend framework. I wanted a deeply typesafe frontend framework, but I felt that Angular was way too heavy and verbose (which I still believe), and that JSX-style templates were messy and encouraged undisciplined coding practices (which I don't really believe anymore). I also loved the pug templating language and whitespace sensitive languages in general (and still do), and loved many of Vue's api concepts such as single file components, simple component event handlers, two-way component syncs, and the slot system.

With all those opinions I set out to make a frontend framework of my own (I know I know), one that from the beginning valued top-to-bottom typesafety, non-magical fine-grained reactivity, and metaprogrammatic transformation to allow nice ergonomic apis. I didn't have any good ideas for a name, so I just punted the name and called it project-f for "project frontend".

I again got it basically working! By the time I was done it was possible to define a component in a single .iron file and compile it to safe typescript. However I realized it was going to be extremely difficult to get anyone to adopt a framework like this if it didn't work nicely with existing tooling such as the typescript language server and things like webpack. So I began working on solving that problem too.

macro-ts (opens new window): 2020-07-09 to 2020-08-20

This is one of the most finished projects I've worked on, and it seems some other people are actually using it. Feel free to read the release blog post describing the project (opens new window).

The goal of this project was to make macros more "first-class", so that things like the thin-ql and project-f dsl's could nicely integrate with the rest of their surrounding project. I was going to start using this compiler wrapper to build a typesafe application bundler, but again realized that it didn't make any sense to hack around such a large and uninterested project as Typescript. The problem was Typescript and their lack of concern for typesafe metaprogramming, so it didn't feel worth it to keep attacking this problem for such little promised improvement.

monads (opens new window): 2020-08-24 to 2020-08-27

This is just the same monads code that was created in ts-std, but with a slightly improved api (it didn't make sense to change the original since it was being used fairly heavily at my employer) with some macro-ts macros included.

validate (opens new window): 2020-08-27 to 2020-10-01

Basically the same as monads, where I improve the api slightly and add some macros. I did also substantially flesh out the api to support more complex ideas like intersection types.

journalism-cooperative (opens new window): 2020-10-13 to 2020-11-03

For a long time I've been interested in effective altruism (opens new window) and logically validated political reforms such as quadratic voting (opens new window). I had finally got frustrated enough with my pseudo-secret and poorly considered technology ideas that I was trying to think of other useful things to do with myself. I had been thinking and writing off and on about ideas for other reforms, and a big one I'd had was for adaptive voting (opens new window) and how it could be used to make member cooperatives much more effective and competitive.

After reading about various companies starting to create new local news companies using email newsletters, I thought that model might be a good fit for a cooperative. Read all about it in this blog post on the subject (opens new window). At first I thought I might try to start the organization myself, and I did some work to make a basic Rust email validation server. But I realized I'm not a good fit to run an organization like that.

traya (opens new window): 2020-12-11 to 2021-02-11

In this project we can see the first hints that I had become sick of unverified code, and was slowly moving toward where I am today. In this repo I was playing with a Coq formalization of basic parsing ideas, ones that could be applied to a more advanced LR version of kreia (bonus points if you know why kreia and traya are related ha).

But what's really happening in this repo is that I'm learning how to use Coq. I was still terrified of the language when I started this work, and I knew I couldn't just do exercises someone else had come up with forever. So I decided some basic parsing theory might be tractable but interesting enough to help me get my arms around Coq. I'm happy to say the process did what I hoped, and I walked away from this work with a lot more confidence.

hopeful-path (opens new window): ~2020-07-01 to 2021-05-24

The start date here is a little fuzzy, since I initially drafted a lot of the essays and notes in a now-deleted repo :facepalm:

After coming up with adaptive voting and finding various ways to apply it to tricky problems, I was increasingly pestered by a sense of urgency to write a book about "how to fix everything" from a political standpoint. The early part of this date range is much less intense, as I occasionally wrote scattered notes and ideas, but at some point I was consumed by the need to just get these ideas out of my head and dove into it headlong. I wrote the bulk of this open source book in about three months, and put it on the internet.

I again wasn't brave enough to share it widely! Quite soon after releasing the first version I began to see big deficiencies in the structure of the book, and again occasionally wrote notes and thoughts about what the next version would look like. I'll touch on this question later.

magmide (opens new window): 2020-08-21 to present

You'll notice how long the magmide repo has been around! Even that early date is likely not early enough, since the same now-deleted repo that held many of the first hopeful-path essays also held a bunch of notes for this project.

After my first foray with Coq I was slowly reading a ton of different resources: things about Hoare logic and separation logic, type theory and the calculus of constructions underlying Coq, different books about Coq such as Certified Programming with Dependent Types (opens new window), the various plugins and systems built on top of Coq such as metacoq, different formalization projects for languages at all different levels of the abstraction hierarchy, and other proof systems such as Liquid Haskell and F* and Lean.

All this reading was necessary, and over time I became more and more convinced we needed a new language. This is where I am today, and I again invite you to check out the Magmide repo (opens new window). The problems in our software stacks go all the way to the bottom! So we need a language capable of fixing them from the bottom up.

---

Looking over all this work I've done, I'm extremely disappointed in myself for being so scared. Almost all the above projects were either completely private or just not widely shared enough to get feedback.

Until today! I've made all these repos public, and have sent messages to people I think might have something useful to say about the projects that actually are worth looking at. I'm done hiding, and I'm committed to working with whoever will help to bring formal verification into the mainstream and use it to solidify our software infrastructure. We can't wait any longer!