Re:Applying TLA+ in cloud systems [video]
by mjb on Tuesday December 15, 2020 @09:43AM
(#25430723)
Looks like a great talk. I'm looking forward to watching the whole thing later.
Jumping forward to the TLA+ section, I very much like the point about how TLA+ enabled precise communication between teams. Writing about distributed algorithms is really hard to do well, and the precision of TLA+ makes it much easier to communicate points in a clear way. This is true of math in general, of course, but my experience has been that many folks are more willing to work through TLA+ code than work through written formal math (and, once you learn it, it's much more approachable in this domain).
Jumping forward to the TLA+ section, I very much like the point about how TLA+ enabled precise communication between teams. Writing about distributed algorithms is really hard to do well, and the precision of TLA+ makes it much easier to communicate points in a clear way. This is true of math in general, of course, but my experience has been that many folks are more willing to work through TLA+ code than work through written formal math (and, once you learn it, it's much more approachable in this domain).
We've been using TLA+ at Amazon for a long time (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...), and of course it was developed at Microsoft. Despite that, it's still quite a small community, so I'm always excited when it comes up.