Very cool post. I like this point particularly: > In this case we can’t assume, in general, that the thread scheduler will assign each thread processor time wi

Very cool post. I like this point particularly: > In this case we can’t assume, in general, that the thread scheduler will assign each thread processor time with uniform probability. That assumption makes even less sense in a fully distributed system with processes running on separate computers connected by a network. I would love to see tools in this space mature some more. TLA+ has had a huge influence on how I approach distributed and concurrency problems, and a large influence on the industry in general. Modelling non-determinism (beyond the 'try all paths' approach), and assigning probabilities to outcomes, seems like the large missing piece needed to model real-world systems and protocols. In systems with limited redundancy, for example, there's always a "transition to a failure state" path which tends to get ignored in modelling with tools like TLA+. That's because these tools can tell you that the whole thing might fail (which is useful), but not the probability that the whole thing would fail (which is significantly more useful).