3 ms·
> The level of trickiness/subtlety of the problems you encounter can determine how much benefit you'll see from TLA+, although I believe people often underestim
by csharptwdec19 6y ago
> The level of trickiness/subtlety of the problems you encounter can determine how much benefit you'll see from TLA+, although I believe people often underestimate it (in a way, all bugs are a result of programmers underestimating the complexity of a problem).
Yep, and a good example is when TLA+ was used against some AWS services [0], it was able to expose bugs that were 35 states deep. To be able to find such a bug in production would require very good tracing most likely; to have a specification detect such bugs before you have even coded the thing is invaluable.
> 2. distributed systems and concurrency are a very common example of subtle algorithms that engineers often encounter and are tricky to get right without help.
I would posit that Distributed systems are typically a category of concurrent systems; just at a different level of abstraction (threads vs nodes)
[0] - https://en.wikipedia.org/wiki/TLA%2B#Industry_use https://en.wikipedia.org/wiki/TLA%2B#Industry_use
- pron 6y ago> I would posit that Distributed systems are typically a category of concurrent systems Absolutely, and so are interactive systems, which are distributed/concurrent between the computer and the human user. In TLA+ all of these are described in the same way, but colloquially, engineers think of them differently, and there are actually good reasons for that, too. E.g. virtually no concurrent algorithms (for a single computer) account for a failure of a single core and its associated L1 cache, but all distributed algorithms do.