2 ms·
TLA+ is an ugly language, just like PlusCal. I'll never understand how people can come to the conclusion that it's fine to have syntax like: * \A p \in people
by blub 8y ago
TLA+ is an ugly language, just like PlusCal. I'll never understand how people can come to the conclusion that it's fine to have syntax like:
* \A p \in people
* acc = [p \in people |-> 5]
* (-- ;) for wrapping PlusCal
* /= for inequality
* /\ for and
* seq1 \o seq2 for append
* and so on
All of these are from the Practical TLA+ book.
Honestly, TLA+ (or PlusCal) looks very impractical. If I want to use mathematical notation I'll do on paper, not write some frankenstein version of it in Eclipse.
At this point the whole syntax should be written off as a failed experiment and they should kindly ask Anders Hejlsberg or Guido van Rossum for help.
- pron 8y agoThat's not the syntax, that's just the ASCII representation. The syntax, which is what you get when the Toolbox presents your spec in pretty-printed form, is: * ∀ p ∈ people * acc = [p ∈ people ↦ 5] * ≠ for inequality * ∧ for and * seq1 ∘ seq2 for append That's fairly standard mathematical notation. In fact, one of the things I enjoyed about TLA+ is that I didn't really need to learn the syntax, as it's so standard. Even the non-standard bits (like alignment that can replace parentheses) are quite intuitive. And if you say, well, I still have to type the ASCII, then you're missing the point. Specifications are not internet rants where you dump a lot of characters on the screen. They are usually quite short, and you spend nearly all your time thinking or reading them.
- brohee 8y agoA good ligature font solves those...