6 ms·

[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to hand

[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.

Jtsummers 6y ago
That's what PlusCal seems to be there to help with. It will generate statements like the above from a more Pascal-ish form.
_alex_ 6y ago
most of the time I need to read it, I use the PDF generation. It turns all the ascii into math symbols. way easier to read
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.
hwayne 6y ago
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt https://github.com/Viasat/salt
- elcapitan 6y ago
  That's interesting, are there more examples of such languages?
  - hwayne 6y ago
    The other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo
- michael_j_ward 6y ago
  wow, that feels extremely more approachable. Are there downsides to using that?
  - hwayne 6y ago
    I've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.
  - pron 6y ago
    I haven't used salt, but the thing to understand is that even when the syntax used is Clojure, the semantics is TLA+'s. So, for example, if you use a Clojure function syntax to define a TLA+ operator, that will not behave like a Clojure function, but like a TLA+ operator, which behaves very differently from Clojure functions. So the symbols on the screen might be more familiar, but their meaning will be different from their meaning in Clojure. I think that is more confusing, which would be a downside, but if you find that more approachable -- great, use that.
barakm 6y ago
I've started working on doing TLA+-style models but using Python as the language for doing so (disassembly and all) with an easier to deploy model checker. Super super early and I'm not quite yet ready to announce it, so don't expect miracles (or post it everywhere) but if you're reading this comment and want to see hacks in this space... https://github.com/timewinder-dev/timewinder https://github.com/timewinder-dev/timewinder
- neolog 6y ago
  How does the performance compare to TLA+? Especially curious if you've run it under PyPy.

Jtsummers 6y ago

That's what PlusCal seems to be there to help with. It will generate statements like the above from a more Pascal-ish form.

_alex_ 6y ago

most of the time I need to read it, I use the PDF generation. It turns all the ascii into math symbols. way easier to read

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.

hwayne 6y ago

We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt https://github.com/Viasat/salt

elcapitan 6y ago
That's interesting, are there more examples of such languages?
- hwayne 6y ago
  The other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo
michael_j_ward 6y ago
wow, that feels extremely more approachable. Are there downsides to using that?
- hwayne 6y ago
  I've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.
- pron 6y ago
  I haven't used salt, but the thing to understand is that even when the syntax used is Clojure, the semantics is TLA+'s. So, for example, if you use a Clojure function syntax to define a TLA+ operator, that will not behave like a Clojure function, but like a TLA+ operator, which behaves very differently from Clojure functions. So the symbols on the screen might be more familiar, but their meaning will be different from their meaning in Clojure. I think that is more confusing, which would be a downside, but if you find that more approachable -- great, use that.

barakm 6y ago

I've started working on doing TLA+-style models but using Python as the language for doing so (disassembly and all) with an easier to deploy model checker. Super super early and I'm not quite yet ready to announce it, so don't expect miracles (or post it everywhere) but if you're reading this comment and want to see hacks in this space... https://github.com/timewinder-dev/timewinder https://github.com/timewinder-dev/timewinder

neolog 6y ago
How does the performance compare to TLA+? Especially curious if you've run it under PyPy.