Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

Parent Full thread

I would say yes. There is nothing that inherently connects TLA+ to distributed systems. It's just that 1. it's general enough to deal with nondeterminism and concurrency that, unlike some other formalisms, it can be easily and naturally used to specify them, and 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. The combination of these two aspects, as well as the fact that the inventor of TLA+, Leslie Lamport, is very well-known for his work in distributed systems, led to TLA+ being popular in that field.

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

TLA+ is relatively easy to learn compared to a new programming language, and you can become reasonably proficient in it in two weeks of self study. The biggest difficulty is unlearning some habits from programming and internalising that while writing a mathematical specification shares some superficial similarities to programming the activities are different in most ways (and fun in very different ways).

> 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

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

> as well as the fact that the inventor of TLA+, Leslie Lamport, is very well-known for his work in distributed systems, led to TLA+

But didn't lead him to come up with decent distributed algorithms. PAXOS is a negative example here for example, where Leslie said that formalization naturally derives such algorithms, but in reality many years and many iterations on the idea from many different researchers and engineers is what led to something actually useful in practice, as PAXOS wasn't, and formalization was by far the least important thing ever.

I'm not sure how you're getting this. In what way is Paxos a negative example? Raft, which is also a take on Paxos, was also formalised in TLA+ by its inventor, as were many other variations on Paxos; in fact, it is hard to derive any non-trivial distributed algorithm, based on Paxos or otherwise, without formalisation. This is true for most subtle algorithms, and distributed algorithms are prime examples of those. Algorithms that had not been formalised on inception, Chord being a famous example of one thought to have been "proven" correct without formalisation were often found to be incorrect once formalised [1]. Not to mention that that work won Lamport the Turing Award.

[1]: https://brooker.co.za/blog/2014/03/08/model-checking.html

Reply on news.ycombinator.com