3 ms·
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+
by dwohnitmok 7y ago
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.
- mjb 7y agoSpeaking 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.
- dwohnitmok 7y agoMakes 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?).