3 ms·
> "deliberately avoids any formal specification or proof" > how is this possibly a selling point? Context. In an overview doc? The informal version is access
by scottlamb 3y 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.
- anentropic 3y agoApologies! I was only blindly responding to the parent comment... FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architecture/election_rsm/#the-leader-election-algorithm-in-blazingmq 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 https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus