|
|
|
|
|
|
by scottlamb
1054 days ago
|
|
|
> "deliberately avoids any formal specification or proof" > how is this possibly a selling point? Context. In an overview doc? The informal version is accessible to more audiences. As the canonical design doc for the system? It's certainly not. |
|
|
FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architecture/elec...
The full sentence reads:
"This section explains the leader election algorithm at a high level. It is by no means exhaustive and deliberately avoids any formal specification or proof."
Which makes a lot more sense.
And as noted in a sibling comment there is actually a TLA+ spec for the leader election: https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus