4 ms·
While I'm reading this, I feel more and more like asking: Am I the only one that finds TLA+ much easier to read and write than PlusCal? It's an odd thing to say
by technion 8y ago
While I'm reading this, I feel more and more like asking: Am I the only one that finds TLA+ much easier to read and write than PlusCal? It's an odd thing to say, with PlusCal positioned as the easier option.
- sriram_sun 8y agoI didn't know about the PlusCal option until I saw Hillel's book and it clicked with me instantly. Might be the damage done by programming. Objectively, PlusCal is a higher level language. So it should be easier than TLA+ right? More specifically, look at https://pastebin.com/cwZaApmH https://pastebin.com/cwZaApmH. The top half is PlusCal and bottom half (after \* BEGIN TRANSLATION) is the translated TLA+ code. PlusCal reads more like pseudocode. Maybe with some more training/effort the TLA+ would be obvious as well.
- hwayne 8y agoOne thing I want to caution is that that's the translation of PlusCal to "raw TLA+". If you were not using PlusCal, you might write it a different way. For example, you wouldn't need a `pc` variable because you could express sending and receiving as short guarded actions.
- pron 8y agoPlusCal is not higher level, it just has constructs that programmers are used to, like assignment, sequential composition, processes and procedures. Even in this particular case the specification would be clearer in TLA+ than in the PlusCal version, had it not been a translation of the latter. For example, the PlusCal version contains an unnecessary and confusing sequential composition of the send and receive bits.
- pwnna 8y agoI found it easier to read TLA+ and easier to write PlusCal. This may be because of "software-first" experience.
- hwayne 8y agoNah, different things click with different people. In my experience more beginners find PlusCal easier to start with than "raw" TLA+, which is why I focus on presenting it first. But plenty of people find raw TLA+ more natural to start with. Use whatever works best for you- once you have one, learning the other is really fast. What matters much more is getting your foot in the door, y'know? Personally, if I'm not writing teaching or workshop materials, I write specs in raw TLA+. Some of that is due to fixable limitations in PlusCal, but a lot is because it's fundamentally a really elegant way of expressing specifications.
- grogers 8y agoPersonally, I keep trying PlusCal and keep going back to plain TLA+. Every time I get bogged down trying to learn it, and instinctively switch back because it's faster (or maybe it just clicks better for me). I got Hillel's book, so I'll probably give it another shot soon. The one thing I really like about PlusCal is that variable updates don't need to be complete, so you don't have to write stuff like: foo' = [foo EXCEPT ![i] = bar]
- deleted 8y ago[deleted]
- marco_salvatori 8y agoAt the risk of being too opinionated, PlusCal is a needless and unproductive diversion. The TLA language and source file structure is mostly standard mathematical notation, using ascii characters. Most people will be familiar already with that mathematical notation before any exposure to TLA. And I wouldn't be able to recommend that people learn just another novel representation for something already known. Learning PlusCal to reason about logical propositions strikes me as comparable to learning an XML notation for manipulating formulas in differential calculus. Yes, we are developers; yes, we are used to XML and, still, ... I don't see how it improves upon writing math. Mathematical notation is a concise, time tested language for enhancing thought. People should use that to their advantage. As an added advantage, unlike PlusCal, facility in the language of propositional logic generalizes widely to other tools used in formal methods, as well as other technical fields.