Design

Why Synod is the way it is. The principles hold together; the decisions record every choice the specification had to make, each with its reason.

Design principles

These principles hold together. When a design cannot satisfy all of them, the design changes; no principle is traded against another.

• Consistency. The same meaning looks the same everywhere.
• One way only. Every meaning has exactly one spelling.
• Canonical code. The compiler accepts only canonical form; synod fmt produces it.
• A tiny language, everything else in packages. The language is a fixed set of words; the standard library is ordinary packages plus a few native phrases.
• Every line reads as pseudocode.
• Writable offline. No LLM is needed to write, check, run or animate Synod. Claude (or any agent) is an accelerator.
• Faithful simulation. Behaviour is simulated, never narrated by an LLM. What you see is what the model does.

Why Synod

Synod is named after the Synod protocol, the core consensus algorithm in Leslie Lamport's paper "The Part-Time Parliament" (ACM Transactions on Computer Systems, 1998; first submitted in 1990). The paper tells it as the story of the parliament of the ancient Greek island of Paxos, whose part-time legislators could agree on decrees although they came and went; today the algorithm is known as Paxos. Lamport later explained it plainly in "Paxos Made Simple" (2001), and in 2013 he received the ACM A.M. Turing Award for fundamental contributions to the theory and practice of distributed and concurrent systems. His "Time, Clocks, and the Ordering of Events in a Distributed System" (1978) and his TLA+ specification language shaped how we reason about such systems. We are grateful for his work, and we hope Synod honours it by making these ideas easier to watch and understand. This repository is the specification of the language that carries his protocol's name.

# from package gossip
Node has
  set Heartbeat to 0
  set Known to {}
  set peers to {}

define [n: Node] start
  time.Every 1s
    set n.Heartbeat to (n.Heartbeat plus 1)
    net.Send (message digest with known n.Known) from n to (random.Pick n.peers)

Decisions

See the numbered table of design decisions.