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.
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...
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.
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.
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 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_interest...) as well as semantic reasons (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.
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.
One of the reasons I'm so bullish on TLA+ is that "the tooling has some issues" is a fixable problem, and the bigger the community, the more likely it is to get fixed.
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.
[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.
But that tool is mathematics. As far as I know -- at least, that's what things were like in my time in school -- when programmers learn mathematics they use standard notation, not their own. When they use the tool called natural language to write documentation, they also use standard notation, not their own, and when they study diagrams they (at least I) prefer looking at a pictures with lines rather than SVG source. I don't understand why a tool that is used by programmers but is nothing at all like a computer program should use computer program notation, and I don't think programmers would prefer reading mathematics differently from everyone else.
I believe the reason this comes up in the first place is that people confuse TLA+'s mathematics with programming (or else why would they even ask something so different from programming to look like programming?). There are specification languages that are, or look like, programming languages; TLA+ came later and is intentionally different -- what's different isn't just the notation but the very meaning of the expressions you write. Why is it different? Because mathematics is simpler than even the most basic programming language -- which has such complex notions like a call stack or evaluation order -- and therefore clearer, and clarity is of the utmost importance in specification. I grew to appreciate that a great deal, and I think that decision makes TLA+ both clearer and more powerful than other specification languages. But you are right -- familiarity to programmers isn't one of it's strengths, but it has many others that, in my opinion, more than make up for that.
I think your judgment is clouded by this insistence that you're doing math rather than something which is squarely in the middle of the cs/math venn diagram. Relational algebra has an accepted notation for left outer-join (⟕). Do you think `I><|` is preferable to `LEFT JOIN` because mathematics™? If I were to sample 100 TLA+ specifications, do you think I would find more people specifying things like paxos and concurrency models, or would I find people doing algebraic geometry and number theory?
If you were to sample 100 TLA+ specifications, you would find 100 descriptions of software systems using mathematical formulas. Physicists don't use different mathematical notation when they write an ODE for a spring or electrical current. Also, I don't understand what notation would be appropriate. Functions in Haskell are much more similar to functions in Java than they are to either operators or functions in TLA+. You could use Java or Haskell notation, but what you'd be using it for would still behave differently from either one, which would only be more confusing. Even when it comes to simple things like conjunction and disjunction, over the past 50 years, programming languages have used at least three different popular representations, while over the last 100 years, mathematics have used one. Why is picking one of the three superior for writing mathematics in TLA+ than picking the one?
Also, you should know that specification languages based on programming languages were the norm before TLA+. TLA+ intentionally broke away from that to offer something different, because Lamport believed it is simpler. I agree, but if you don't, you can use the specification languages that preceded TLA+, like Isabelle and Coq. So you're going to the one language that tried to make things easier by changing things up and asking, why did you change things up? Despite all that, after a three-day workshop, programmers use TLA+ to specify large and complex software systems, something that those who learn the programming-language-based specification languages do not, so perhaps Lamport was right.
It is mathematics for anyone who wants to describe discrete and hybrid systems, including programmers. But I believe mathematics is used by mathematicians, physicists, engineers of many kinds, and biologists for many different things -- that's what mathematics is for -- and they all use pretty much the same notation. Also, and this is important, there is no standard programming notation for mathematics. TLA+ operators and functions simply don't behave like subroutines in any programming language. I think using the same symbols, but with a different meaning, would be more rather than less confusing.
For example, when in TLA+ you specify the function, f, from the integers to the integers such that f(x) = -f(x), you've obviously defined the zero function; I'm not aware of any programming language that works like that. While TLA+ doesn't have macros, the value of x = 3 ∧ Foo(x) = 5 might not be equal to x = 3 ∧ Foo(3) = 5, and I'm not aware of any non-logic programming language that works like that, either, at least not without some hidden complexity (simple mathematics also doesn't work like that, but this is because TLA+ is a modal logic), and logic programming languages have syntax that isn't any more familiar to non-logic programming language programmers than TLA+'s.
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.
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 -- 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.
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.
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/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.
A very useful article for the non-noob learner of TLA+!
> This is the launching point into refinement, or using an entire specification as the checked property of another spec.
We use the term "refinement" for those more special cases where `A` and `B` are both canonical formulas (`Init ∧ □[Next]_vars ∧ Fairness`), or, at least, both contain an initial state predicate and at least one box-action clause, but when learning, it's important to understand that there is nothing special about refinement in TLA+ from a mathematical point-of-view. Every formula in TLA+ describes a class of behaviours. The key general point to learn is that TLA+ does not distinguish between specifications and properties; they're just classes of behaviours that we can call a "system property" or a "system specification" based on how we psychologically think of it. The TLA+ formula `A ⇒ B` means that `A`'s behaviours are contained in `B`'s, and can be read as "specification A implements specification B" or "specification A satisfies property B" or "property B is an abstraction of property A" or "specification B is a generalisation of property A." All of these are just words used to describe the abstraction/refinement relation that's the very core of TLA+. So this is refinement, and `□[A]_vars` is an entire TLA+ specification, as is `□P` (it is true that TLC cannot check the specification `□(x ∈ 1..3)` but it can check the equivalent formula `x ∈ 1..3 ∧ □[x' ∈ 1..3]_x` but that doesn't make the simpler formulation any less of a valid and complete TLA+ specification of a system).
It's worth noting that while it's not anything special from a math point of view, there's a lot more technique involved in specifying and verifying `ImplSpec => AbSpec`, which is why it's considered a more advanced topic.
I find it easier to chunk and read "always eventually" - i.e. the combination "[]<>" - as "progresses" and "eventually always" - i.e. the combination "<>[]" - as "stabilizes".
So []<>A can be read as "A progresses" and <>[]A as "A stabilizes".
hwayne's Learn TLA+ [0] is a very approachable introduction and survey. Lamport's TLA+ course [1] is an excellent follow on after going through Hillel's course. That link also includes the book itself.
I would add an excellent introduction by Scott Wlaschin on YouTube called "Building confidence in concurrent code using a model checker."[0]
Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two chapters of that (free) book before you do anything else, but you may feel like you're wading through mud if you don't start writing simple specs and watch his or other tutorials by chapter 5. Most of his example specifications (Chapter 5, Chapter 11) design a memory interface for a computer, and they suppose you are familiar with basic computer architecture. If not, you'll have to learn TLA+ while learning how a memory interface works at the same time, which takes dedication.
The appeal to me of TLA+ is using set theory and first-order predicate logic to describe any system, from a poker game to a shopping trip to a computer program - anything at all where the next state depends on the history of the system after a set of initial states. The TLA+ Toolbox IDE has a TLA+ model checker called TLC that can test your logic, and that is particularly useful for a complex concurrent or distributed system if you ever design one.
