Design notes

The type system that
audits the protocol

Writing Raft in MoonBit leaned on the language's types. Where a conventional implementation uses a struct field and a convention, MoonBit uses a sum type and an exhaustive match - and the compiler refuses to let a case go unhandled. Three times, filling in a case the code left implicit turned up a real latent bug. Two of them were safety violations.

Method: we fixed the implementation, never the assertion. Every bug below is pinned by a regression test that fails before the fix and passes after.

Bug 1 · Election & State-Machine Safety

B1Two leaders in one term

Raft's whole promise is that a committed entry is permanent. That rests on Election Safety: at most one leader per term. The reference step path had a gap - it never dropped a response stamped with a term below the receiver's own.

The failure

A VoteResp from an old term, reordered late by the network, was counted into the current tally - enough to manufacture a false majority and elect a second leader in a term that already had one. A stale AppendResp could likewise inflate a follower's progress and over-commit. Both break the guarantee the log rests on.

The regression test

b1_stale_term_wbtest.mbt replays the reordered stale response. Before the fix it observes is_leader() true on a second node and a commit index of 3 where 0 is correct; after the fix, both hold.

The fix makes "how does this message's term compare to mine?" a value you must destructure - so "it's older" cannot be silently skipped:

priv enum TermRel {
  Stale      // msg.term < ours - ignore requests, DROP responses
  Aligned    // msg.term == ours
  Ahead      // msg.term > ours - step down first
}

fn step(self : RaftNode, m : Message) -> Array[Message] {
  match self.term_rel(m) {
    Stale   => match m.payload {
                 // a response from a dead term proves nothing
                 VoteResp(_) | AppendResp(_) | HeartbeatResp(_) => return []
                 _ => /* reply with our term so the sender updates */
               }
    Ahead   => self.become_follower(m.term())
    Aligned => ()
  }
  // … only messages that passed the classifier reach the handlers
}

In a conventional implementation the term comparison is a chain of ifs; forgetting the response case compiles cleanly and ships. Here the match on TermRel and the nested match on Payload are both exhaustive: leave the stale-response case out and it does not build. The bug becomes unrepresentable.

Bug 2 · Storage contract

S2Compacted or just unavailable?

When a leader asks storage for an entry the follower needs, the answer decides the next move: if the index was compacted away, send a snapshot; if it is simply past the end, wait. The old storage returned the same empty answer for both - a None that conflated two states needing opposite responses.

Before - one None for two worlds

fn term(i : UInt64) -> UInt64? {
  // compacted? out of range? caller
  // cannot tell - and guesses wrong
  ...
}

After - the states are distinct by type

suberror StorageError {
  Compacted
  Unavailable
  SnapOutOfDate
  SnapshotTemporarilyUnavailable
}

The read path now raises the precise variant; storage_bridge.mbt catches it and either ships a snapshot or backs off - no guessing. TestStorageTerm, TestStorageEntries and TestStorageCompact assert the distinction that the boolean answer used to erase. (A third fix, S1, corrected apply_snapshot wrongly advancing the HardState commit index - a conventional implementation leaves it untouched.)

The through-line

Types that erase whole classes of bug

Both fixes share a shape: a place where Go collapses several distinct situations into one under-specified value - a bare term integer, a None - and MoonBit forces them apart into a sum type the compiler makes you handle. The bug is not caught at test time; it is made impossible to write.

Messages are one enum

Every request is paired with its response in a single Payload. A transport moves them without knowing what any means; a handler cannot receive a shape the type forbids.

Roles are a closed set

Follower / Candidate / Leader - every transition is a match over three cases. A new state can't be bolted on without the compiler pointing at every site that must account for it.

Errors carry their reason

StorageError replaced a boolean that discarded exactly the information the caller needed. The recovery decision reads off the variant.

Where to next

Run it, read it, change it

The same consensus core powers the in-browser demo and the deterministic simulator used throughout these notes. Drive a cluster yourself from the quickstart, browse every public type and method in the API reference, or read the source package by package - quorum, tracker, raftpb, confchange, storage, log and core.

▶ Watch the invariants hold Browse the API

The type system thataudits the protocol