4 ms·

First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TL

by pron 6y ago

First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is no convenient formatter for HTML yet, only PDF. Second, TLA+ is very much designed for writing mathematical specifications that are much smaller than most programs (a TLA+ specification with ~2000 lines of maths is very big, while a program with 2000 lines of code is quite small), that are then read and contemplated a lot. Several hours of thought for every line of maths is pretty normal for TLA+. Writing maths [1] is absolutely not like programming, both for ergonomic and workflow reasons (https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interesting_twitter_discussion_on_tlas/fbkoprq/ https://old.reddit.com/r/tlaplus/comments/edqf6j/an_interest...) as well as semantic reasons (https://old.reddit.com/r/tlaplus/comments/enencr/yet_another_example_that_tla_is_math_not/ https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...). Easily the hardest thing in learning TLA+ (which is a tiny, and extremely simple formal maths language) is understanding the difference between programming and simple mathematics, and it takes work to internalise that. The syntax, which is pretty much standard mathematical notation, more or less, helps. [1]: TLA+ is roughly the discrete analogue to ODEs describing a continuous engineered system.

TTPrograms 6y ago
Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.
- pron 6y ago
  It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+. Anyway, it's not what you're supposed to read. The vast majority of TLA+ is readable to someone familiar with ordinary mathematical notation within two to ten minutes of training (if you know temporal logic, then almost all of TLA+ is readable within minutes). See e.g. this complete (and very sophisticated in its use of advanced TLA+) specification, written at Arm, of CPU speculation side-channels: http://www.procode.org/cachespec/ http://www.procode.org/cachespec/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.
  - hwayne 6y ago
    This messes me up when I'm writing actual LaTeX because I keep writing `\A` instead of `\forall` EDIT: Also that spec uses a lot of really interesting techniques, such that doing a breakdown would be a good Blub study. Off to the typewriter!
lakecresva 6y ago
I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_<<x, y>>` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the difference between specification and programming.
- pron 6y ago
  It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific operator; I think writing maths in a less familiar notation would be less appealing and require more training [2]. I did say that the tooling is missing an HTML formatter, which is why some bloggers prefer posting the source rather than the typeset maths. Still, the syntax -- standard mathematical notation -- isn't for everyone, just as Python or Java syntax isn't for everyone, either, and yeah, the tooling has some issues. Also, yes, it is my opinion that if you focus on an editing environment -- which I like, BTW -- for short mathematical texts that you rarely actually edit compared to most other kinds of texts, then you're missing something quite fundamental about TLA+ (if you don't like the editor, pen and paper is another nice editing environment for TLA+; it's also a standard maths editing environment, but it feels more than 20 years old). But that's just my opinion, and you don't have to agree with it one bit, just as I don't have to agree with yours. I'm not the boss of TLA+, nor its official ambassador, just someone who likes it, and you should form your own opinions. You really shouldn't take what anyone else you don't personally know says on the internet too seriously. I do like TLA+ a lot, which is why I'm exited to talk about it, but if you like it for completely different reasons or even don't like it at all, that's perfectly fine, too. My enjoyment of TLA+ or practical gain from it isn't harmed by you not liking it. It is fun to talk about something you like with others who like it, too, but if we all liked the same things the world would be pretty boring. Many people dislike the things I like, and sometimes I even like arguing with them. But it's not my mission to get you to like the same things I do. [1]: That notation is due to https://en.wikipedia.org/wiki/C._I._Lewis#Logic https://en.wikipedia.org/wiki/C._I._Lewis#Logic [2]: E.g. TLA+ functions don't behave like programming language subroutines; using the same syntax might be more familiar, but also more confusing because the text would look the same but mean something different.
hwayne 6y ago
It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has synonyms for common operators. You can write `implies` instead of `=>` if you want, which makes the teaching experience much smoother. If I could have students use `&&`, `||`, and `!` instead of ⋀ ⋁ ¬ that'd cut out a lot of early friction. This is also why I "pythonize" the TLA+ tokens during talks. Trying to explain the math syntax gets in the way of explaining the core ideas.
- pron 6y ago
  I agree it's a barrier for beginners, but I think this is a good barrier, which makes the next, bigger ones, easier to overcome. A step is also a barrier, but I'd rather face more, lower steps than fewer taller ones. By the time you realise neither operators nor functions work at all like functions from programming, the syntax has helped to put your mind in a "this is not programming" mode. Also, || and && are almost universally used in programming languages today, but they weren't thirty years ago, and might not be thirty years from now (Zig doesn't use them and neither does Nim), and even in C, C++, and Rust they have similar but subtly different meaning than | and & involving evaluation, a concept that TLA+ doesn't have -- now there's a more interesting and more important unfamiliar TLA+ thing -- while ∨ and ∧ have been used much longer than that and aren't going anywhere. So every person might prefer something that's already familiar to them, but there is no alternative that's really universal. If you go to Wikipedia -- say, https://en.wikipedia.org/wiki/Logical_connective https://en.wikipedia.org/wiki/Logical_connective -- they use "TLA+ notation," not C notation. Anyway, there are other, and more important, things in TLA+ that are much less familiar from programming (e.g. there's no evaluation) than how to write logical or, and still TLA+ has been more successful at teaching programmers to specify more complex systems more quickly than any other specification language I'm aware of.

by pron 6y ago

TTPrograms 6y ago

Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.

pron 6y ago
It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+. Anyway, it's not what you're supposed to read. The vast majority of TLA+ is readable to someone familiar with ordinary mathematical notation within two to ten minutes of training (if you know temporal logic, then almost all of TLA+ is readable within minutes). See e.g. this complete (and very sophisticated in its use of advanced TLA+) specification, written at Arm, of CPU speculation side-channels: http://www.procode.org/cachespec/ http://www.procode.org/cachespec/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.
- hwayne 6y ago
  This messes me up when I'm writing actual LaTeX because I keep writing `\A` instead of `\forall` EDIT: Also that spec uses a lot of really interesting techniques, such that doing a breakdown would be a good Blub study. Off to the typewriter!

lakecresva 6y ago

I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_<<x, y>>` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the difference between specification and programming.

pron 6y ago
It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific operator; I think writing maths in a less familiar notation would be less appealing and require more training [2]. I did say that the tooling is missing an HTML formatter, which is why some bloggers prefer posting the source rather than the typeset maths. Still, the syntax -- standard mathematical notation -- isn't for everyone, just as Python or Java syntax isn't for everyone, either, and yeah, the tooling has some issues. Also, yes, it is my opinion that if you focus on an editing environment -- which I like, BTW -- for short mathematical texts that you rarely actually edit compared to most other kinds of texts, then you're missing something quite fundamental about TLA+ (if you don't like the editor, pen and paper is another nice editing environment for TLA+; it's also a standard maths editing environment, but it feels more than 20 years old). But that's just my opinion, and you don't have to agree with it one bit, just as I don't have to agree with yours. I'm not the boss of TLA+, nor its official ambassador, just someone who likes it, and you should form your own opinions. You really shouldn't take what anyone else you don't personally know says on the internet too seriously. I do like TLA+ a lot, which is why I'm exited to talk about it, but if you like it for completely different reasons or even don't like it at all, that's perfectly fine, too. My enjoyment of TLA+ or practical gain from it isn't harmed by you not liking it. It is fun to talk about something you like with others who like it, too, but if we all liked the same things the world would be pretty boring. Many people dislike the things I like, and sometimes I even like arguing with them. But it's not my mission to get you to like the same things I do. [1]: That notation is due to https://en.wikipedia.org/wiki/C._I._Lewis#Logic https://en.wikipedia.org/wiki/C._I._Lewis#Logic [2]: E.g. TLA+ functions don't behave like programming language subroutines; using the same syntax might be more familiar, but also more confusing because the text would look the same but mean something different.

hwayne 6y ago

It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has synonyms for common operators. You can write `implies` instead of `=>` if you want, which makes the teaching experience much smoother. If I could have students use `&&`, `||`, and `!` instead of ⋀ ⋁ ¬ that'd cut out a lot of early friction. This is also why I "pythonize" the TLA+ tokens during talks. Trying to explain the math syntax gets in the way of explaining the core ideas.

pron 6y ago
I agree it's a barrier for beginners, but I think this is a good barrier, which makes the next, bigger ones, easier to overcome. A step is also a barrier, but I'd rather face more, lower steps than fewer taller ones. By the time you realise neither operators nor functions work at all like functions from programming, the syntax has helped to put your mind in a "this is not programming" mode. Also, || and && are almost universally used in programming languages today, but they weren't thirty years ago, and might not be thirty years from now (Zig doesn't use them and neither does Nim), and even in C, C++, and Rust they have similar but subtly different meaning than | and & involving evaluation, a concept that TLA+ doesn't have -- now there's a more interesting and more important unfamiliar TLA+ thing -- while ∨ and ∧ have been used much longer than that and aren't going anywhere. So every person might prefer something that's already familiar to them, but there is no alternative that's really universal. If you go to Wikipedia -- say, https://en.wikipedia.org/wiki/Logical_connective https://en.wikipedia.org/wiki/Logical_connective -- they use "TLA+ notation," not C notation. Anyway, there are other, and more important, things in TLA+ that are much less familiar from programming (e.g. there's no evaluation) than how to write logical or, and still TLA+ has been more successful at teaching programmers to specify more complex systems more quickly than any other specification language I'm aware of.