4 ms·
One advantage of PlusCal is that it’s super easy and convenient to experiment with which operations need to be atomic and isolated than it is in raw TLA+. In pl
by mjb 8y ago
One advantage of PlusCal is that it’s super easy and convenient to experiment with which operations need to be atomic and isolated than it is in raw TLA+. In pluscal, you can just move labels around, and try out “if the system could crash between these two operations, would it still be correct?” and similar questions. You obviously can do that in TLA+, but it’s more work.
Also, for me, TLA+ and PlusCal have huge value as documentation and communication tools. It’s not about whether I would prefer to read TLA+ or PlusCal, it’s about which my intended audience would prefer. Different situations lead to different choices.
Also, TLA+’s syntax is (in my entirely subjective opinion) needlessly weird, and makes the semantics somewhat less approachable.
- pron 8y ago> Also, TLA+’s syntax is (in my entirely subjective opinion) needlessly weird, and makes the semantics somewhat less approachable. For me it's the opposite. I find programming language (and PlusCal) syntax weird, though not needlessly so, as programming languages are necessarily extremely complex. TLA+ is the cleanest, simplest, most natural syntax I've yet seen for describing computations (and it is not surprising that research into "natural" programming for non-programmers in languages like Eve has ended up with something similar), and it's hard for me to imagine any other syntax with clearer semantics. But obviously this is a matter of personal taste. I don't particularly like PlusCal (and I find TLA+ easier to understand), but I've used it for low-level concurrent algorithms.