Pure Consensus in a World Full of Failure
Distributed consensus protocols are notorious for doing people’s heads in. Machines fail and networks lag, which are unfortunate consequences of entropy. Without loss of generality we can assume that the machines despise us, our only hope is to enchant them with correctness proofs, and that we must somehow convince them that safety and liveness are our primary moral concerns.
This talk introduces a new Haskell implementation of Raft, deconstructed as a menagerie of cooperating abstractions for communication, storage and control. A pure protocol description allows local testing and validation of exactly the code that is run on a production cluster. We pause to consider denotational semantics for, like, 30 seconds (“What does it mean to be a protocol?”) before tumbling into the rabbit-hole of code that deals with machines who can’t even agree on what time of day it is.
All attendees will receive a free monad.