What are formal systems?

A programmer-y exploration of their weird and cool nature

I work at Metabase, and I like my job. If you want to work at Metabase and like your job, come apply to work here! I program in Clojure (though the frontend folks work in TypeScript), everyone is smart, and it’s 100% remote with people all over the world. The code is open source, and it’s used by UNESCO. Apply now.

What are formal systems?

When I’m drafting my book, I often get a glimpse of the underlying structure the ideas I’m presenting are built on. These ideas seem so important. But alas, they’re often very abstract and not directly relevant to the skills I’m trying to teach to a particular audience. This newsletter and my podcast are a way to write/talk about those ideas to a more sympathetic audience.

My book is about domain modeling. One ideal to strive for when building a domain model in code is to construct it as a formal system. When I first got that idea, I do what I typically do, which is to start writing about it. But soon I realized that I didn’t really know what formal meant in that term. I did some research. And it’s a really important idea, so I’m going to share my understanding with you.

Before my research, if you asked me what formal system meant, I would tell you that it’s about being rigorously defined, as in “let’s get a formal definition.” But that’s not it, really. Yes, formal system are rigorously defined, but they’re a lot more like programming languages than just “good definition.” Let’s look at an example:

In predicate logic, a kind of formal logic, we can assign variables to a few concepts:

• Jim - the protagonist of this story

• Pizza - the plot device

• Likes - the character development

• Eats - the action

Then we can talk about Jim, like this:

\(Likes(Jim, Food) \implies Eats(Jim, Food)\)

This means that if Jim likes a food, he eats it. Now what happens if we also throw this into the mix?

\(Likes(Jim, Pizza)\)

Jim likes pizza. We can then imply that:

\(Eats(Jim, Pizza)\)

Jim eats pizza. Surprise ending.

Well, okay, it’s not a very interesting story. But it does give us everything we need to define formal system, the real plot of the story. Mathematicians will define it like this:

A formal system consists of:

• symbols (valid characters/tokens) — Jim, Likes, (, ⇒, …

• statements (valid arrangements of symbols) — Likes(Jim, Pizza)

• mechanistic rules (for deriving new statements from existing statements) — the rule that lets us derive our ending

• axioms (statements that are true implicitly)

I think of it in programming terms. The first two items (symbols and statements) are the syntax. The last two (mechanistic rules and axioms) define the semantics.

There’s something about formal systems that is powerful and paradoxical. There’s a strange combination of meaning, meaninglessness, and machine-like coldness that somehow makes them more powerful. And that’s why I find them fascinating, just like programming itself. It’s just electrons moving through a circuit, yet somehow it does meaningful work. Where does the meaning come from? (Hint: It’s us.)

First, the syntax defines a structure, like an Abstract Syntax Tree. An important part of the syntax is that there are symbols that are neutral. These are the variables. We defined variables like Jim and Pizza, but as far as logic is concerned, they could be A and B. Logic doesn’t care about Jim or pizza. Likewise, your compiler doesn’t care what you name your variables, nor does the chip it runs on. And this is important. The variables are only linked to human meaning through their names and other connections to real-world things.

However, some parts of the syntax are meaningful to the system. The structure itself is meaningful (as in F(A, B) indicates a predicate called F with arguments A and B). And some of the symbols have meaning (⇒ means implication). The meaning comes from their use in the mechanistic rules, somewhat how a syntax-driven interpreter would work. The structure of the statements is pattern-matched in the derivation rules, which leads to new statements. The term formal refers to the importance of the structure in defining meaning.

I find this mix of meaningless symbols and meaningful symbols to be a beautiful puzzle. Yes, there is a certain elegance to formal systems like propositional logic. A handful of meaningful symbols (logical connectives) and a few inference rules can ensure you only derive valid arguments. But there’s something more than just elegance at work. There’s something to their limited meaning that makes them practical. Logic wouldn’t work if you tried to include all humanly felt meaning, so you only include a tiny subset that you trust to work. Yet it can find new, if simplistic, results.

One interesting exercise is to find the minimal set of meaningful symbols that can express all the others. In propositional logic, this is the NAND connective (NOR works, too). The SK combinator calculus is Turing complete. And you can derive both S and K from the iota combinator! So iota, just one symbol (and using the lambda calculus rule of application) is Turing complete.

Similarly, Lisp is very minimal (at least the original Lisp). It is defined with three kinds of symbols:

1. Atoms (alphanumeric sequences)

2. (

3. )

The syntax also requires spaces between atoms to distinguish them. The syntax defines two kinds of values:

1. Atoms

2. Lists

Super minimal! The inference rules are also simple:

1. An atom’s meaning is either a number (if it’s all digits) or it’s a symbol, in which case its value is looked up.

2. A list’s meaning is determined by the first value in it.

   1. There are certain symbols with special meanings, like lambda or cond.

   2. Other symbols are looked up and applied like functions to the arguments.

This is such a simple formal system, yet it builds up an entire programming language. I’m leaving out that you probably have to define a lot of the functions yourself in some other language (like machine code), but even that number is small. In other words, Lisps are bootstrapped. Lisps today are more complicated, but they still maintain some taste of the simplicity of the original.

What I think is cool is that programming languages are essentially formal systems. They have all the ingredients. Their semantics are defined by the compiler, which defines them as a translation into another formal system, the machine code. Strangely, machine code does not have any non-meaningful parts. Anything you can express in machine code is meaningful to the semantics of the chip. The only hint of a meaningless thing is that it operates on numbers that themselves are meaningless to it, except in as much as it knows how to do arithmetic on them and fetch memory at a numeric address. They are abstract quantities that represent values meaningful to us. So we can say 1 means Jim and 2 means pizza.

I feel compelled to mention the book Gödel, Escher, Bach right now, for some reason. I have read only a few pages of it, but it’s probably a more playful and complete exploration of the strangeness of formal systems than I can possibly do. Just wait until you see what self-reference in a formal system does to it!

The challenge with using formal systems is in modeling a real-world scenario. It’s an art to translate Jim and his tastes into logical statements such that you can derive new meaningful statements from it. The derivation, once the statements are written, is quite trivial. This challenge of encoding the meaning is one reason why proofs are hard even when something seems obvious. By the way, the art of encoding a set of real-world scenario into a program is known as domain modeling. What are the meaningful parts you want to capture from the domain, and what parts are you leaving up to the humans for meaning?

There’s also a cool balance between minimalism of the system and human habitability. Sure, it’s very elegant that NAND is complete. But just look at the statements you have to write to do anything! They’re unreadable. It’s very hard, as a human, to wrap your intellect around them. Structure dominates. Perhaps you can eventually learn to read it, with time, but you’re mostly just counting parentheses. Check out this expression using the iota combinator:

\(ι(ι(ιι))(ι(ι(ι(ιι))))\)

So clear! (not)

There’s a tradeoff between number of symbols and length/structure of statements. We want to select a set of symbols we can easily juggle in our minds (not too big) that are, at least metaphorically, meaningful to the concrete world we live in. Making the story about Jim and pizza is something we can relate to with almost no effort. Jim eats foods he likes, he likes pizza, so he eats pizza. It’s obvious (I believe) because it taps into the social parts of our brains. We want symbols like ⇒, ∧, and ∨. We can understand them. Software design is often about this tradeoff: Do we inline the code or do we extract a function and give it a meaningful name? Do we want longer code or more symbols?

The last cool thing I want to mention is that this is the key to stratified design and metalinguistic abstraction. In stratified design, each layer defines new meaningful symbols for the layer atop it to use (relying on the underlying lambda calculus rules of inference). But in metalinguistic abstraction, you define an entirely new formal system, with new rules of inference, that hopefully lets you express your problem more easily than lambda calculus. Think a rules engine or SAT solver.

Well, it’s time to conclude. Formal systems are a neat mix of meaning and meaningless parts. The meaningless parts are like holes where we can fill in our own, human meaning. We want to find a set of meanings we can use to derive the answers to our questions. That is not easy. And finding the balance between the number of meaningful symbols and the structure is an art. These are some of the underlying questions we face every day when we program. The questions never go away, but the practice of domain modeling points you to a reliable source of answers: The domain itself.