On Algebra, and What It’s For
I still don’t have a good answer for what the field of “algebra” is. Formally, an algebra over an operad is a structure where you can interpret a collection of operations as acting on the structure. More concretely, if you’re defining an algebra over a field, you’re defining a vector space with some kind of bilinear product. Neither of these helps anyone understand what algebra is, because while every object you study is some kind of algebra, you aren’t working at that level when you’re doing an exercise. But it leads nicely into nLab’s characterization:
Algebra is the manipulation of symbols without (necessarily) regard for their meaning, especially in a way that can be formalized in cartesian logic. It is often seen as dual to geometry. While modern algebra has ties and applications nearly everywhere in mathematics, traditionally the closest ties are with number theory and algebraic geometry.
I want to draw attention to without regard for their meaning. The whole field admits, in its own self-description, that the symbols come first and the meaning comes after, if it comes at all. Similarly, a computer is a machine that pushes symbols around without regard for their meaning, and so is a Lean proof, and so is a sufficiently committed algebraist, and the relationship between these three things is what I’ve gotten to live out.
This is written for my technical but also nonmathematical friends. Much of the examples are simple, mostly because I have forgotten the more technical ones. I don’t know how to memorize the things I know I care about beyond ruthlessly going back (there’s an argument that relearning is cheap, but memorization is obviously so much stronger…). This is me looking back.
Two Reals
Most students meet the real numbers twice. The first construction is Dedekind cuts, where a real number is the set of all rationals strictly less than it. The ordering is just set inclusion, which is satisfying due to its naturality. The second construction uses Cauchy sequences: a real number is an equivalence class of rational sequences whose differences converge to zero. This one is “uglier” but more immediately useful, as it lets you multiply and divide without too much pain, and it generalizes, as it’s the completion of the rationals with respect to a metric, and you can complete other things by the same recipe.
Both constructions stage infinity in a particular way. A Dedekind cut is an infinite set. A Cauchy sequence is an infinite sequence with an infinite tail for each epsilon. If you hand a machine two reals built either way and ask it whether they’re equal, the machine has to answer: I would need forever. Not because the algorithm is slow, but because the question is the kind of question that doesn’t have a finite witness. To know two infinite objects agree, you have to check infinitely many places they could disagree.
This is the first thing I want a reader to sit with. There is a fundamental object, the real number, which mathematics talks about constantly, which every undergraduate manipulates, which appears in every equation a physicist writes down, and which a computer cannot in general decide the equality of. The object is perfectly well-defined. The reasoning about it is perfectly rigorous. And at the level of the machine, the level of can I run this, there is a gap, and the gap is not a bug in any particular implementation. It’s a property of the object.
Lean4 has a keyword for this. If you write a definition that the compiler can typecheck but not execute, such as something that involves the axiom of choice, or excluded middle, or just an honest piece of mathematics that has no operational content, you need to mark it noncomputable. Lean will let you reason about it, but it will not let you call it from anything that’s supposed to actually run. The keyword is the language admitting, in the most unembarrassed way I’ve ever seen a formal system admit anything, that there’s a difference between I can talk about this and I can do this. GasStationManager’s SafeVerify tool, which checks Lean proofs for the usual sins, deliberately does not catch noncomputable at the .olean level, because the keyword is just how it is.
I find this simultaneously strange and calming. I’m not sure I can fully justify why without waxing poetic, so I’ll just say that a language that has a word for the place where its syntax outruns its semantics is a language that has thought about what it is supposed to do.
Computational Algebra
In my mind algebra is a very French subject, as the big names might suggest: Bourbaki, Galois, Grothendieck, Serre. The word itself is from الجبر, al-jabr, the reunion of broken parts, and for centuries the field meant the theory of polynomial equations and not much else. It only really expanded after the Fundamental Theorem of Algebra in the early nineteenth century, after which it stopped being about solving equations and started being about the structures that solving equations makes you notice (specifically, how it relates to geometry).
Then, in the late seventies, three things came together that had been brewing for a while. Buchberger’s algorithm for Gröbner bases, originally from his 1965 thesis under Gröbner himself, became widely known. Collins’s cylindrical algebraic decomposition arrived in 1975. Lazard’s work on solving systems of polynomial equations matured around the same time. By the end of the decade you had, for the first time, a real toolkit for running algebraic geometry rather than just reasoning about it. The constructive content of nineteenth-century algebra finally had executables.
Hilbert’s Nullstellensatz, in its effective form, is the theorem I keep coming back to here. The bare statement is that if a system of polynomial equations has no common solution, there’s a witness proving it has no solution. The interesting question, the one mathematicians have been chasing for a century, is how big the witness has to be. Hermann gave the first bound in 1926, and it was doubly exponential, which is another way of saying that the witness existed but you would never find it. Brownawell tightened it to something polynomial in characteristic zero in 1987. Kollár generalized it algebraically, and Sombra refined it further. There is a chain of mathematicians, spanning a century, who cared enough about whether the witness was findable, not just whether it existed, to spend significant parts of their careers grinding down an exponent. This is what I mean when I say algebra feels constructive. The field has people in it who treat the question, can we actually do this, as a first-class question, not a tidying-up afterthought. I believe combinatorics and theoretical CS contain this too, and I have enjoyed studying them as well.
Last year my tutor handed me a paper on cyclotomic identity testing and I spent afternoons when I should have been studying for collections trying to fill in every line of the first three sections. The setup is the most computational thing I have ever seen in pure algebra. You have a polynomial with integer coefficients, but you don’t get it as a list of coefficients. You get it as a directed acyclic graph whose vertices are addition and multiplication and whose leaves are monomials, and the polynomial is what the graph computes. A ring is a structure with addition and multiplication, so you might as well draw the operations as a graph and let the graph be the object. The vertex set is the algebra. The graph is the system. And the question is whether the polynomial it computes evaluates to zero at a primitive root of unity. You can prove that the absolute value of the norm of the algebraic integer that the circuit computes is at most the order of exp(exp(exp(s))), where s is roughly the number of edges plus the bit length of n, and the doubly-exponential blowup is the whole reason the problem is hard. The algorithm that decides it works by reducing the entire computation modulo a carefully chosen prime, doing arithmetic in a finite field where the roots of unity actually live, and using the fact that if the reduced answer is zero then the prime had to divide the norm, which gives you, with high probability, a certificate of non-zeroness you can hand someone. It is a beautiful piece of work and it lives entirely inside the spirit of effective Nullstellensatz: the question is not whether the answer exists, it is whether you can actually find it. And the punchline is that the proof that the algorithm runs in polynomial time depends on the Generalized Riemann Hypothesis, which nobody has proven. We have an algorithm. We can run it. The proof that it is fast depends on a conjecture the world has not yet figured out how to settle. The syntax-semantics gap shows up again, one level up: we can write the proof down, we can typecheck the proof, and the thing the proof leans on is a thing nobody knows just yet.
I love this feeling working in a tractable system and knowing what matters. I love it the way you love a particular kind of walk outside with the sun on your face. And I have to be honest about which parts of algebra I love and which parts I only respect, because the field is large and the parts pull in different directions. I love the parts where the symbols and the machine meet. I respect, from a distance that is starting to feel permanent, the parts where the symbols have left the machine behind. I have just started reading Serre’s Local Fields, and it is beautiful, and I can see the cathedral it’s a doorway into. Some of my professors would say Neukirch’s Algebraic Number Theory is full of abstract nonsense, and they don’t mean it as praise. I don’t think it’s nonsense. I think it’s what algebra becomes when it follows the symbols all the way to wherever the symbols want to go, sometimes even including places no machine can follow. André Weil, writing to his sister Simone from a French prison in 1940, described the deepest experience he had in mathematics as catching a glimpse of an analogy between number fields and function fields. It’s the joy of recognizing the same structure in two places it had no business being. That’s beautiful.
Hardy, in A Mathematician’s Apology, made the famous case that the best mathematics is beautiful precisely because it’s useless, and that number theory was his favorite field because nothing in it could ever be applied. He was wrong about the empirical claim (RSA happened) but the aesthetic position is coherent, and a lot of mathematicians live inside it. I don’t know if I do. The thing I find beautiful in algebra is not its distance from use but the fact that, when you do it right, the distance collapses. A Gröbner basis is a piece of pure structure and also a thing you can hand to a computer. The effective Nullstellensatz is a theorem about pure existence and also a promise that the existence is reachable. An algebraic circuit is a polynomial and also a graph in memory. Hardy’s beauty is the beauty of an object behind glass. The beauty I’m chasing is the beauty of an object you can pick up.
Haskell
I learned Haskell while I lived in Oxford. It’s a statically typed, functional, lazy language, invented in 1990, with maybe a half-dozen companies using it nontrivially at any given time, such as Standard Chartered’s strategies group, Tsuru Capital in Tokyo, Mercury, IOHK, a couple of others, depending on the year and who’s hiring. The ecosystem is small and the people in it are, on average, the kind of people who would rather get the type right than ship the feature, which is both why the language is loved and why it stays small.
The thing about Haskell is that if you write down the type of the function carefully enough, the function writes itself. The smallest case: a function of type a -> a, where a is any type at all, must be the identity. You have no other guarantees about a, so there’s nothing else you could possibly do. This generalizes more than you’d expect. A surprising number of useful functions are the unique inhabitant of their type, or close enough that the type narrows the function down to a handful of candidates and you pick the one that doesn’t loop forever. Writing Haskell is, much of the time, a process of stating what you want precisely enough that the thing you want becomes the only thing you could have written.
This is the same activity as algebra. I mean this almost literally: you are pushing symbols around under constraints, and the constraints are tight enough that the symbols start to move themselves. What the function does when you eventually run it, or more concisely, the meaning, is downstream of the syntax, and the syntax was downstream of the type, and the type was downstream of what you were trying to say. It is the most algebraic experience I have ever had at a keyboard, and the keyboard is part of the point. In algebra proper you can have the same experience, but you have to do all the bookkeeping in your head or on paper, and the bookkeeping eats your attention. In Haskell the compiler does the bookkeeping. You get to spend your attention on the part where the symbols decide what they want.
I wrote a bare-metal operating system in Haskell as a final project for a course. It runs on a Raspberry Pi Zero, boots from an SD card, gives you a shell with eighteen commands, talks to two NRF24L01 radio modules over SPI for wireless communication, runs green threads on a 100Hz timer with a round-robin scheduler, and has a Lisp interpreter embedded in it whose REPL can blink LEDs and read GPIO directly. It’s about five thousand lines of Haskell, thirteen hundred of C, and three hundred of ARM assembly. I don’t recommend it as a way to learn operating systems but I recommend it as a way to find out what happens when a language designed to abstract the world away meets a piece of hardware that demands to be addressed directly, in bytes, at fixed addresses, with no margin for politeness.
The thing I want to tell you about is the garbage collector. I couldn’t use GHC because GHC’s runtime depends on a Linux underneath that doesn’t exist on bare metal, so I used MicroHS, a tiny Haskell compiler by Lennart Augustsson that compiles to SKI combinators and has a runtime small enough to bootstrap from C. MicroHS’s GC walks the heap and follows pointers. On Linux this is fine, because address 0x00000000 is unmapped, and if the GC ever tries to dereference a null pointer the OS catches it and crashes the program loudly and obviously. On a Raspberry Pi with no OS underneath, address 0x00000000 is the ARM exception vector table, which contains perfectly valid-looking bytes that can be interpreted as a heap node pointer if you are a garbage collector who doesn’t know any better. So the GC would walk into the vector table, follow what it thought was a chain of allocations, and silently corrupt memory in a pattern that depended on what interrupt handler had most recently been installed. The bug was in the language’s runtime, not in any code I had written. The fix was teaching the GC that the heap had a lower bound and to refuse to follow pointers below it.
I want to put this next to everything else in this essay. The GC’s source code is correct on every machine where address zero is unmapped. The semantics of follow this pointer depends on a fact about the world the source cannot see. The syntax of the GC and the semantics of the GC come apart at exactly the place where the abstraction it was written against (the existence of an operating system) stops being true. Lean has a keyword for this. Computer systems have a debugger and three days of staring at the wrong memory map. (There was also an off-by-one in the peripheral region. The EMMC controller lives at 0x20300000 and I had mapped through 0x202FFFFF, which is the kind of mistake that takes longer to find than to describe.) Same gap. Different building.
The other thing I want to tell you about from that project is the page table. An ARMv6 1MB section descriptor packs a physical address, an access permission, a domain, a cache policy, and an execute-never flag into a 32-bit word, and in C you set them with shifts and masks and pray you got the bit positions right. In Haskell I made a record type with the fields named, and the access permission was its own four-constructor sum type (no access, privileged only, user read-only, full access), and the cache policy was its own three-constructor sum type, and the type system simply made it impossible to construct a page table entry with a nonsense permission. I never had to remember which bit pattern meant which access mode because I never wrote down a bit pattern. The type was the specification and the specification was the code. This is the algebra side of computer systems showing up exactly where you’d want it to: the place where the cost of getting the bits wrong is highest is also the place where pushing symbols around under tight constraints is most useful.
However, Haskell is lazy, which means it doesn’t evaluate anything until something forces it to, which means a lot of the work of running a program in Haskell is happening at a level the program itself doesn’t quite see. The IO monad is the place where the language admits, similarly to Lean’s noncomputable, that the world exists and the world is going to require sequencing. Outside of IO, Haskell is pretending the world doesn’t exist, and most of the joy of writing it comes from how convincing the pretense is.
The pretense has limits. You can’t easily handle hardware interrupts. The concurrency story is built on green threads, which are not real parallelism. The set of possible behaviors of a concurrent program is exponential in the number of interleavings, and typing concurrent programs well is one of the hardest problems in language design, and Haskell does not solve it, it just gives you better tools for not making it worse. Race conditions are where syntax and semantics come apart in the same way that real-number equality and noncomputable are places where syntax and semantics come apart, and the fact that the same gap shows up everywhere I look is part of why I started thinking the gap might be the actual subject.
Trusting Trust
In 1984, Ken Thompson gave a Turing Award lecture called “Reflections on Trusting Trust.” The argument is short. He describes a way to modify a C compiler so that when it compiles the Unix login program, it inserts a backdoor letting Thompson in. Then he describes a way to modify the compiler so that when it compiles itself, it inserts the backdoor-inserting code into the new compiler. After one round of this, you can delete the malicious source code entirely. The compiler binary will keep producing backdoored login programs, and backdoored compilers, forever, and an inspector reading the compiler’s source will see nothing wrong, because there is nothing wrong with the source. The malice lives in the binary and reproduces itself across generations of the binary, invisibly.
Thompson’s conclusion is that you cannot trust code you did not totally create yourself. No amount of source-level review is sufficient, because the thing reading the source is itself a program, and that program could be lying. The only honest position is to know that somewhere underneath every system there is a layer you didn’t write and can’t fully verify, and to live with the layer rather than pretending it isn’t there.
I want to put this next to Lean’s noncomputable, and next to the undecidability of equality for real numbers, and next to a garbage collector walking into an exception vector table at three in the morning, and let the reader notice what they have in common. In all four cases, you have a formal system that looks like it gives you semantic guarantees. The source is clean, the proof typechecks, the real number is well-defined, the GC is correct on every machine the GC has ever run on, but there is an irreducible gap between what the syntax promises and what the semantics can deliver. In the math case the gap is a curiosity for logicians. In the proof-assistant case it’s a keyword. In the kernel case it’s a memory map. In the systems-security case it’s a place where adversaries live. The gap is the same gap. It is the gap between what you can write down and what you can run, what you can prove and what you can check, what you can trust and what you have to trust anyway. The recent unease about large language models, where we have built something whose syntax is fluent and whose semantics is a stranger to us, is, I think, another instance of the same shape, and we’re going to spend the next few years discovering that the shape is older than we knew.
The people who work in systems are the people who have made peace with the gap. Not solved it. Not closed it. Made peace with it, in the sense that they treat it as the working condition of their craft rather than as a scandal that has to be cleaned up before the real work can begin. This is the part of the systems sensibility I find I want to spend more time around.
Two Modes of Beauty
I broadly believe there are two modes of beauty in the world. The first is the beauty of things that don’t need us: the patterns in nature, the structures in mathematics, the parts of algebra that would be true whether or not anyone had ever noticed them. Hardy’s beauty. Weil’s beauty. The cathedral you can see from a distance.
The second is the beauty of the human project. We invented music. We invented dancing. Someone, at some point, invented the sidewalk, which is one of the most extraordinary objects in the world if you stop to consider it. It’s a strip of stone whose only purpose is to let strangers pass each other without quite touching, and in passing, briefly, to share a city. Baudelaire, writing about Constantin Guys in The Painter of Modern Life, described the figure of the urban observer as someone who is “away from home and yet feels at home anywhere; to see the world, to be at the very center of the world, and yet to be unseen by the world,” a man who has become “a kaleidoscope endowed with consciousness.” That’s the second beauty. The beauty of having made a thing that lets a human being feel that way.
I used to think these two modes were opposed, and that I had to pick. Elaine Scarry, in On Beauty and Being Just, argues that beauty has a generative property, that one of the things beauty does is create the desire to replicate it, to make more of the beautiful thing in the world, to bring others to it. If that’s right, then the two modes aren’t opposed. The first kind of beauty is the kind you recognize more than make. The second kind is the kind you make more than you recognize. And the act of recognizing a structure and the act of making more of it are the same act, performed in different materials.
A friend of mine worked on Google’s central TCP/IP stack. He sat down and focused. And then he commented out one line and sped up every web request Google performs. Stealing the hypothetical from Gavin Leech (https://gleech.org/stopping), imagine that this saved a quadrillion milliseconds a day across all users. That would be eleven years of human life, every year, given back to the people whose web requests are now faster. He said it was the most valuable week of work he ever did. That commit is, in Scarry’s sense, a beautiful object, as it is a recognition of a structure (the stack had an inefficiency) and a making (a world with more time in it) performed simultaneously, in a medium where the recognition and the making cannot be separated. It is almost the same act as proving a theorem about Gröbner bases. It is almost the same act as bounding the norm of an algebraic integer computed by a circuit. It is almost the same act as writing a function whose type already knew what the function was. It is almost the same act as deleting six lines from a garbage collector and watching a kernel stop corrupting itself. It is different, because it touches the human project. But it is almost the same.
This is the thing I am trying to say. The reason I love algebra is not that it is timeless and useless and beautiful behind glass. It is that, when you do it right, it is the place in mathematics where recognition and making are the same act. And the reason I am moving toward computer systems is that systems is the place outside mathematics where recognition and making are most the same act, where the gap between I see this structure and I have made more of it in the world is the smallest, and where the people working in the field have already made their peace with the syntax-semantics gap that I find I cannot stop thinking about.
Coda
I have been feeling the cognitive load of all the algebra I’ve been studying. I still know almost nothing. I have just started Serre’s Local Fields, which is the foothills of the foothills. I believe the cathedral is beautiful and I am grateful to have stood inside it for a while. I am not going to spend my life there. The part of it I love is the part that has not lost contact with the machine, and the parts that have lost contact, however beautiful, are not where my hands might want to be.
Maybe I am biased toward learning new things for fun. Maybe I am a fanboy of Eric Zhang, who seems to live in systems the way I want to live in systems. I don’t fully know. Maybe I just want to climb new mountains instead of struggle alone through the foothills.
You’re only given a little spark of madness, and you have to follow it where it actually leads, not where you think it should lead. I can remember being a child running across the slightly wet fields of Cambridge to give a lecture on model theory. I remember standing in Colorado and realizing a recurrence held for a proof and emailing my coauthor about the proof. I remember the first time two Pis on the same desk passed a typed Haskell value to each other through a 2.4GHz radio, and the moment of feeling that the type system had successfully spanned a piece of empty air. All three of those memories are about the same thing. I just didn’t have a word for the thing yet.
I think the word is clickity-clackity, for when the types click-and-clack together correctly. I think it is more honorable than it sounds, and I think the place where it lives most densely is a few buildings over from where I have been sitting. I am going to go see.
PS – I’m going to try and finish Local Fields by Serre, and I’m going to try and come up with cool systems projects. It’s kind of hard to know what you can do until you do more of a thing! Also, I want to work more with other people. Working by yourself is lonely.
Also, things come with pain and hunger as you do them. I’m not sure how to deal with them. I think you just do.
