[combatentropy]

Is TLA+ pseudocode? It doesn't actually do anything, right? Your example with updating servers, it will never actually update the servers, right? After you try it out in TLA+, you still have to write the real code in some other language, like Bash.

If so, then isn't there still a risk of bugs in your Bash program, from typos, leaving out something from the TLA+ plan, or otherwise miscopying it?

If so, TLA+ does less than I thought. But I can see how it might be useful to work out a complex algorithm and scan it for holes.

[hwayne]

Yeah, TLA+ just verifies the spec, not the actual code. You still need to write tests and use code review and the like.

[combatentropy]

Okay, that makes sense. Thanks!