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+

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). We've been using TLA+ at Amazon for a long time (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext 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.