> it's a huge breath of fresh air as a formal documentation language.
Yeah! When I started with TLA+ I was mostly enamored with model checking and proofs. Those turned out to be useful, but the unexpected use of being a really great way to write crisp descriptions of protocols and algorithms is probably a bigger benefit. That's one of the reasons I tend to choose PlusCal over "raw" TLA+ these days: it's easier for others to read and engage with.
After publishing this paper, I had a great email conversation with Leslie Lamport about this use of TLA+. We talked about TLA+'s use as a "low ambiguity documentation" tool, and some of the cases where we've been able to resolve conversations about ambiguities in our implementation because we had the TLA+ spec to fall back on.
Fascinating; did you guys stick almost exclusively to PlusCal (except presumably for writing invariants in TLC)?
I'm quite partial to just using straight TLA+ for everything because it's both what ultimately it all desugars to anyway and because it makes what you put in TLC and what you write for your spec the same language. Plus once you're in the mindset of TLA+, the syntax of PlusCal has always seemed more of a distraction than anything else, but it does seem that PlusCal is a lot less scary for an experienced developer with no TLA+ experience.
Speaking only for myself, because we don’t have anything approaching a standard here, I do about 60% PlusCal and 40% straight TLA+.
Mostly the tradeoffs are the ones you mentioned. If I was the only audience of what I was writing, I’d pick TLA+ every time, but for a broader audience PlusCal can make this stuff much more approachable.
Makes sense. One last question while I still have you here. What's the TLA+ adoption look like within AWS? I imagine it's probably still only a small minority of teams, but exactly how small are we talking (you guys are the only ones, 2-5, 5-10, or 10s?).
Just a tiny nitpick: there is no need to qualify TLA+ with anything (especially "raw", as "raw TLA" is already used for something else). There's TLA+ and there's PlusCal, a language that compiles to TLA+. True, TLA+ also refers to the gestalt of the TLA+ toolbox, but whether you're referring to the tools or to the language is often clear from context. E.g: "At my company we use TLA+, but we prefer writing specifications in PlusCal." "At my company we also use TLA+, but we write the specifications in TLA+."
Yeah! When I started with TLA+ I was mostly enamored with model checking and proofs. Those turned out to be useful, but the unexpected use of being a really great way to write crisp descriptions of protocols and algorithms is probably a bigger benefit. That's one of the reasons I tend to choose PlusCal over "raw" TLA+ these days: it's easier for others to read and engage with.
After publishing this paper, I had a great email conversation with Leslie Lamport about this use of TLA+. We talked about TLA+'s use as a "low ambiguity documentation" tool, and some of the cases where we've been able to resolve conversations about ambiguities in our implementation because we had the TLA+ spec to fall back on.