> 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
> 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.