[c0achmcguirk]

Man it looks really cool to use this in an enterprise. It seems like you'd need a lot of support to introduce it into an Enterprise environment. Ramp-up time for learning and it looks like it runs really slow, so you'd need buy-in for the runtime too.

Any advice for those of us who'd like to introduce this to a team rather than play with it on our own?

[colanderman]

Learn it on your own first before trying to foist it on others. I'm on the cusp of seriously introducing use of TLA+/PlusCal at the startup I'm at, and having worked through (and had success with) modeling a couple real-word concurrent systems I have designed here, I have a very different perspective how to use TLA and explain it to co-workers than when I first started using it.

(For example: it's tempting to think of variables as some sort of communication channel – they're not. And fairness can be hard to conceptualize until it's put to a real-world use.)

Definitely use PlusCal. It's a little more to learn, and a little more restrictive, than straight TLA+, but most TLA+ specs you write will end up looking like the output of PlusCal anyway, and the PlusCal version will be much more compact and easy-to-follow. Just remember that PlusCal is not like any other programming language; especially the "await" statement can throw newcomers off (it's not like "await" in other languages).

[hwayne]

The way it worked out for me was to first learn it on my own, then model a buggy system at work, then demonstrate how it finds a bug. It's one thing to explain the ideas, another to see it actually run and produce an error trace that maps to a problem in the code.