I recently found myself with some time, so I dedicated 2 weeks to pick up OCaml’s basic patterns-of-thought by writing an event-simulator that demonstrates a classic consensus protocol (Paxos). The goal was to implement something familiar as a proxy to gaining intuition around something unfamiliar. ~4 weeks laterScope-creep is inevitable for personal projects. This also doesn’t count the months between finishing the code and finishing the writing — some consulting work intervened, and the series sat until I could give it the attention it needed. The open git history chronicles the actual timeline., the project is at a stage where I can focus on talking about it…
This series documents the design thinking, decisions made and moments of friction as a story-arc where my relationship with the compiler changes from adversarial to collaborative. What starts as noise — type errors that I couldn’t explain, constraints that felt arbitrary — eventually becomes something I could work with. Towards the end of the arc, I even find myself applying the compiler’s discipline in places where it has nothing to say.
Happily, this work is also a small step towards my long-term goal of creating meaningful teaching artefacts (e.g. guided projects with effortful learning curves) for FOSS ecosystems. Teaching people how to teach themselves is difficult because learning is a deeply personal habit and not every skill is learned the same, but a reliable start to exploring that is to make my own learning style visible.
Figure 1: 🙙 Photo of the Milky Way seen from the Gobi desert by Daniel Kordan, retrieved 🙛
In this series, we’ll first spend some time world-building so that we can bake algorithm invariants and helpful assumptions into narrative analogues that will help guide our understanding. Consensus algorithms are famously difficult to learn, so we shall pick the simplest version of the Paxos protocol and its safety guarantees for the first cut of the simulator. This helps to maintain focus on what the language and its tooling can teach us. Before we write any code, we will establish some design grammar that shapes how we architect our simulator. Finally, we cover some anecdotes on how the compiler influenced my own implementation.
To explain his consensus algorithm, Leslie Lamport1 chose the narrative backdrop of part-time parliamentarians on the ancient Greek island of Paxos. Since this is an OCaml-project, we keep things Camel-themed and draw inspiration from the nomadic Tuaregs that travelled across the Saharan desert for trade.
Part I starts with
building that world: where multiple caravan groups have to come to a decision — a consensus — despite unreliable environments that may impede communication.
Table 1:
The Paxos- and Tuareg-themes are analogous
Paxos-themed
Tuareg-themed
Structure
Parliamentarians with private opinions
Caravans with private commitments
Actors with local state
Messengers between parliamentarians
Couriers shuttling parchment
Messages between nodes
Senate sessions convening & adjourning
Desert sun rising and falling
Logical time
Scribe recording the decrees
Chronicler observing from afar
Simulator interface
To keep the focus on the safety-argument and simplify the implementation-scope, we will tactically omit some behaviours from this v0 implementation:
Single decision (consensus attempt), not a replicated log
We will prioritise demonstrating safety within a single decision so that per-node state is small enough to trace by hand. Nodes will keep an append-only log but we’ll defer log-replication to v1.
No failure-detection
For example, we won’t use timeouts to detect failures because detection as a goal is not important for Paxos’ safety argument. This also removes timing as a source of non-determinism.
No log-reconciliation
Nodes will crash and restart, and they will never lose state. However this durability of state will be basic since we won’t build the ability for nodes to bring laggards up to speed i.e. log-reconciliation.
Modelled concurrency
Time will be modelled deterministically as a single-threaded loop. Concurrency would be modelled as an interleaving of events for v0 so that everything is easy to trace.
The original paper proves safety rigorously but deliberately leaves progress mechanisms unspecified — treating those as implementation choices rather than protocol requirements. Our omissions here extend that same instinct: v0 keeps the safety argument airtight and defers everything else.
The narrative backdrop should provide sufficient context to appreciate the need for consensus protocols and how to achieve safety. Details on the fundamentals of Consensus Algorithms, deeper literature and some commentary are in
the Addendum.
We complete Part I without writing a single line of code because the project’s objectives and design constraints should be influencing the implementation rather than the language constructsOCaml’s powerful type system allows users to do sophisticated type-magic to fit their need for expression. It feels good to wield but also makes it easy to overdo it — that’s what we discover in Part II when we try to enforce state machine invariants and have to curb our enthusiasm.that we are free to play with.
The
design rules we establish make us disciplined when separating concerns so that there are clear evolution-paths beyond the v0 implementation of our simulator.
Table 2:
The grammar rules that shaped the architecture before any code did
Rule
Why
Possible to evolve to
1. Nodes talk to each other only by exchanging messages
Message-passing is the only way to interact and an instance of a Bus becomes the single channel for communication. We can trace cause-and-effect by watching a single queue instead of chasing multiple call-stacks.
Supporting a real transport protocol (e.g. IP) requires touching one module instead of every actor.
2. Time moves in discrete, inspectable steps
Every “tick” is loggable, diff-inspectable, and replayable. We don’t have to fight sources of nondeterminism such as the wall-clock.
A wall-clock or multi-threaded driver can be dropped in later without touching actor logic
3. Events are deterministic and replayable
Every run reproduces from its inputs, so that bugs in the simulator implementation are easy to squash by avoiding any race conditions.
Opens the door to record/replay testing and, eventually, fuzzing over event sequences. We can be confidently chaotic, later.
4. Actors are independent. No actor reaches into anyone else’s state
Encapsulation is enforced by the module boundary so that a leak of control responsibilities can never be compiled.
New roles can be added, or one role split into several, without auditing every existing actor for hidden coupling.
5. The world can be paused, rewound, and fast-forwarded
Forces simulator state to be a value, instead of keeping a history of mutations.
Sets up a debugger/inspector, and property-based tests that make simulator behaviour easy to trace.
We expect our implementation to be shaped by our design grammar more so than the OCaml language.
Part II implements the grammar and hits three places where the compiler pushes back.
The setup for all three: a node wears three hats at once — Proposer, Acceptor, Learner — each its own sub-state machine, all live simultaneously. That’s what turns the type questions below into real design decisions rather than syntax trivia.
Table 3:
Three movements in the relationship with the compiler
Movement
The pressure
What it taught
Obeying
When wiring the subsystems together, the compiler refused to unify two types that looked identical to me — the first of two module-boundary snags. The second snag cost more: in order to satisfy a signature that I’d defined too rigidly, I’d been carrying converter functions that shuffled identical fields back and forth.
A module signature is an access-control boundary, but I was treating it more like a type hint. Making the type abstract in the signature let the equality be induced rather than declared. The boilerplate evaporated on its own.
Negotiating
To make illegal state transitions unrepresentable, I reached for a GADT. However those same state types carry [@@deriving sexp, yojson] preprocessor tags so that every transition can be snapshotted — and ppx deriving assumes every constructor returns one uniform type, which is exactly what a GADT refuses to do.
The more type-safe the runtime model gets, the less safe the serialisation boundary gets. Replayability is the point of a simulator, so the failwith arms stayed — known, bounded debt with a resolution already sketched out.
Internalising
Movement 2’s restructuring had a side effect: layering state by role gave each sub-state its own accumulator, which quietly made the old message-inbox redundant. With the inbox gone, every side-effect converged on one function. That was emergent behaviour, I hadn’t designed it like that.
A mutation boundary appeared with no compiler forcing it. The discipline held anyway, because the compiler’s habits of attention — shape of data, direction of flow, where mutation is allowed to live — felt intuitive to me at that point.
The compiler sings, you learn the songs, and eventually you find yourself humming them in places it isn’t.
Narrative backdrop, design forces, abstract grammar, constraints before constructs. Personal narrative on linguistic relativity and what programming languages teach us. No code.
My observations and intuition on some core concepts revolving around this space that may help fast-track other learners. It also aims to funnel readers to actual canonical work that others have done.
Parts
I and
II are complete, while III is in the drafting room for a while more. If you’d rather start with some consensus fundamentals first, then the
Addendum is self-standing for that.
Suggested Reading Paths
Different strokes for different folks: people of different profiles may prefer their own way to read this series:
If you are \(\ldots\)
\(\ldots\) you care about
then try starting with \(\ldots\)
someone interested in how engineers learn and make design decisions — pedagogues, mentors, the curious — even if you don’t consider yourself a technical person
the why behind design: forces, analogies, constraints
Part I — no code, all design thinking. Wanders into linguistics, learning science, and the cognitive residues that programming languages leave behind.
an experienced programmer outside the OCaml world — you build systems, you’ve used a few languages, you want the architectural substance juxtaposed with the code and see it in a seemingly esoteric language
the how: trade-offs, type-system lessons, cross-language perspectives
Part II’s three design pressures — opens with enough context to stand alone. Part I’s
Abstract Design Grammar is worth a look if the design constraints intrigue you.
someone that works in or around the OCaml ecosystem — you’re evaluating the engineering, the taste, the self-awareness
the what: implementation quality, honest debt, maturity of judgement
Part II directly, focusing on the
design pressures. Part III’s debt ledger will be the most candid section about where the architecture falls short.
someone interested in the distributed systems space, especially the consensus content
the substance: quorum intersection, where the variants actually differ, and what a v0 does and doesn’t guarantee
the
Addendum — it’s the depth-layer and reads standalone.
Part II if you want to see the protocol as it was built.
If you have feedback or ideas on making this series clearer, more demonstrative, or more useful — please
reach out to me or open an issue here.
The legendary Leslie Lamport laid the foundations for managing chaos in distributed systems. The Paxos algorithm was published in the 90’s as “The Part-Time Parliament”, which built on his earlier work around the space. ↩︎
Paxos is used as a learning substratePaxos is hard to understand and harder to implement right. This project keeps the scope to single-decree Paxos — narrow enough to be tractable (~2 weeks) and deterministic enough to verify cleanly.in this series. This addendum hosts my observations and intuitions on some core concepts revolving around this space that may help fast-track other learners. It also aims to funnel readers to actual canonical work that others have done.
This is Part II of
a series on learning OCaml by writing a Paxos simulator. We build on Part I’s
abstract grammar and witness how subsystems take shape from it — guided, as it turns out, by the OCaml compilerI’m sure the magical source within the compiler is rooted in the underlying Hindley-Milner Type system which expects the programmer to exercise clearer type-discipline in exchange for superior inference capabilities that feel like an extension to the programmer’s own mind. I’ll put up a few words about what that experience has been like in Part III, coming soonitself.
This is Part I of
a series on learning OCaml through building a Paxos simulator. Here, we stay away from the code entirely and focus on listening closely to the forces that will shape the architecture.
