3 ms·
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 t
by tyu2 6y ago
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.
- Tomis02 6y agoCorrectness dictates algorithms. That's what TLA+ helps you with.
- pron 6y agoBut TLA+ is used to shorten development and help with algorithm performance.
- BenoitP 6y ago> 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." [1] https://blog.acolyer.org/2014/11/24/use-of-formal-methods-at-amazon-web-services/ https://blog.acolyer.org/2014/11/24/use-of-formal-methods-at...