> Which is directly at odds with needing TLA+, because if you do need it, it means the complexity of the algorithms is so great, that you won't be able to keep them in your head and understand every aspect of their performance to make something work well.
I don't think this is correct.
What TLA+ allows us to do is be more creative in our design and choice of algorithms, while allowing the computer to help us reason about whether the choices we're making still result in a system that is correct. "Correct" in in this context means two things: "safe" as in it doesn't lose or corrupt data, and "live" as in it eventually makes progress without deadlock or other blockers. That doesn't capture "meets the SLA" or "fast enough for real use" or even "tolerates gray failures". All of those are critical properties indeed - but unless you have fundamental safety and liveness you're never going to get those properties anyway. You might think you have them, but then you'll have a bad time eventually.
So TLA+ (and similar tools) aren't a complete solution to the problem, but they are an exceptionally useful one. Fundamentally, they're useful because distributed and concurrent protocols, even very simple ones like 2PC, are wickedly difficult to reason about clearly. Computers can help us reason, and specification languages can help us communicate clearly about our reasoning.
That's the thing, performance should dictate the algorithms, not the other way around and TLA+ can't make this process any easier, only harder. I get it's not the case at AWS, where distributed services AWS thinks customers might want is what dictates the choices, but this is an exception, not the rule and unless someone wants to work there they have no reason to be doing it this way, especially not for educational purposes learning distributed systems.
> performance should dictate the algorithms, not the other way
You want correctness first, and performance second. But these two are very much intertwined. And knowing exactly where the boundary is will help you co-design them.
Some AWS engineers have said the following[1]:
"TLA+ [...] giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness."
I don't think this is correct.
What TLA+ allows us to do is be more creative in our design and choice of algorithms, while allowing the computer to help us reason about whether the choices we're making still result in a system that is correct. "Correct" in in this context means two things: "safe" as in it doesn't lose or corrupt data, and "live" as in it eventually makes progress without deadlock or other blockers. That doesn't capture "meets the SLA" or "fast enough for real use" or even "tolerates gray failures". All of those are critical properties indeed - but unless you have fundamental safety and liveness you're never going to get those properties anyway. You might think you have them, but then you'll have a bad time eventually.
So TLA+ (and similar tools) aren't a complete solution to the problem, but they are an exceptionally useful one. Fundamentally, they're useful because distributed and concurrent protocols, even very simple ones like 2PC, are wickedly difficult to reason about clearly. Computers can help us reason, and specification languages can help us communicate clearly about our reasoning.