TLA+ is hard to learn (2018)
surfingcomplexity.blog
surfingcomplexity.blog
For a start, you almost always have two languages in one file - a mixture of 'TLA+' and 'PlusCal' with the latter written in comments and used to generate more TLA+. And although they're separate languages, they're close enough any blog post or search looking for TLA+ has a good chance of actually being about PlusCal and vice-versa.
And every document can be presented two ways - you can write a TLA+ document in ASCII, or take it through a LaTeX-style conversion to make a PDF. So for example, what appears as ⋃ in some documentation might be typed as \cup
That makes a lot of this stuff almost ungoogleable. Go ahead, try and find what ⊑ does or what \bigcirc does. And if you do manage to find a document explaining how to do what you want to do, 50% of the time it tells you ∘ is the operator you want - but not how to type that in.
And it's very easy to make specs that will take forever to validate - and often tough to tell what change made it so. For example, if you simulate four independent processes that count to three, it'll evaluate all the ways those processes could be interleaved in a fraction of a second. But if you increase that three to ten? The model checker will run and run and run. Do you need to leave it to run over night? Wait the age of the universe? As far as I can tell, the only way to know is to wait, and the only way to figure out the cause of the slowness is to undo the changes to your file until it starts checking in a reasonable time.
So while it's a powerful tool, and capable of doing some things that really can't be done any other way, convincing other people of the tool's merits can be tough.
While some people prefer writing PlusCal, I don't think it's the majority. Most people I know just write TLA+. PlusCal is more suitable for "code-level" problems, like specifying low-level operations on concurrent data structures.
As to your point about TLC's sometimes surprising behaviour, I agree, but "mysteriousness" is common in software tools. These are things that are learned through experience. One way to estimate how things are going, even with no experience, is to look at the graphs of newly discovered states that the Toolbox draws. If they're trending down, you're in the process of converging; if they're still going up -- you're not.
Given N deterministic sequential processes with M steps each, the total number of possible behaviors is `(NxM)!/M!^N`. So for 4 processes that count to 10 each, that's `40!/10!^4`, or 4.7 * 10^21 behaviors. If they count to 3 each, that's just 370,000 behaviors.
But I agree that there needs to be a way to type latex Symbols quicker. The Lean Community did this quite well: hovering over a symbol in the docs gives you the correct ascii name.
My guess is that if syntax is improved, a lot of people will give it a shot.
But it is certainly true that languages for writing mathematics often have syntax that's different from languages for writing computer programs, but the question is, would writing mathematics in programming syntax make learning it significantly easier for programmers?
There are certainly many who make the argument that it would -- including some experienced TLA+ users -- but I think there are two points against it:
1. While it might make understanding easier on the very first day, mathematical formulas simply do not mean the same thing, or "behave" in the same way, as programs do -- neither operators nor functions behave the same way as subroutines do, not even the same way "functions" in pure-functional programming languages like Haskell do [1] -- which, on the third week and on actually makes matters more confusing, and,
2. Just as when you want to find some answer about some programming topic, it helps that the answer is in some syntax you know, almost all materials that are relevant when learning and using TLA+ -- say, you want to look up De Morgan's laws on Wikipedia -- are written in the same mathematical notation.
At the end of the day, what you write in TLA+ is mathematical formulas, and the standard mathematical notation is the most familiar and popular syntax for that task.
[1]: https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...
The issue with mathematical notation is more practical one. Most programmers do not deal with maths (and notation) on a daily basis. TLA+ is a tool. If the tool is encouraged to be used in the field by programmers to model their systems, then it should "adjust" to their needs.
This means:
1. Better Debug-ability
2. Easier syntax
3. Better error messages
(I do not know how to do these and do not want to sound it as trivial)
This is where I want to make a subtle point: It does not have to be on par with mainstream language. I am not saying it should be as easy as Python/Go/Java. Solving for some of the low-hanging fruits would have disproportionate improvement in usability.
(A lot of ppl find parsing C++ templates & Rust generics jarring, let alone mathematical notations)
Another example of tool: https://www.wolframalpha.com/
It has both natural language input and mathematical notation as well (you see these options right below the search bar)
Click on any of the examples: https://www.wolframalpha.com/examples/ They are self explanatory for most I assume.
Even a simple "ForAll" instead of the symbol "∀" goes a long way (in my book) https://reference.wolfram.com/language/ref/ForAll.html
The Mathematical Notation is THE universal language of Logic, Set Theory, Functions etc. which are the mathematical underpinnings of Computer Science and Programming. This is what all Engineers need to be familiar with. Programming languages are incidental in this case and are merely used for syntactic expressions of Mathematical Concepts. This is as it should be and the reason Leslie Lamport (the inventor of TLA+) settled on this specific notation. Please see his interviews/videos on Youtube for more details.
In my own case i started by grasping/studying the basics from the following books;
* Software Engineering Mathematics by Woodcock and Loomes.
* Understanding Formal Methods by Monin.
* Introductory Logic and Sets for Computer Scientists by Nimal Nissanke.
* Mathematical Notation: A Guide for Engineers and Scientists by Scheinerman.
This allowed me to start studying Specifying Systems by Leslie Lamport which is the main book for TLA+.
PS: User "pron" to whom you replied to has a nice 4-part series on TLA+ which i have linked to in another post in this thread. He really knows this subject :-)
> I am not saying it should be as easy as Python/Go/Java.
I think it's already significantly easier than all of them already for someone who has no knowledge in programming and/or modelling with mathematics. But programmers need to know that they're not learning another programming language, but a completely new skill.
> They are self explanatory for most I assume.
Yes, but only because I already know what the symbols mean. But if I wanted to learn about any of those subjects, the materials would not be using Wolfram syntax but mathematical notation, so I'd have to learn it, anyway.
Why did Wolfram choose that syntax, while TLA+ (or Coq, or Agda, or Lean) chose a more mathematical one? Because they're used for different things. Wolfram is for quick calculations you feed into the computer. TLA+, OTOH, is supposed to take maybe hours to think about each line, and then, what you'll be doing with it most of the time is not feeding it to the computer but reading it. After a while, mathematical syntax is less strenuous to read than Wolfram syntax, especially when you might have hundreds of lines of maths. The think/read/write ratio of TLA+ is very different from any programming language -- and even Wolfram -- so it doesn't make sense to optimise for the same things.
> Solving for some of the low-hanging fruits would have disproportionate improvement in usability.
Yes, but I don't think syntax is one of those things. TLA+'s syntax is not only rather standard among similar languages and close to the syntax used in study materials, but actually helps.
One of the syntax-related things that I think might help is for the editor to replace the input ASCII with real TLA+ syntax in Unicode as you type.
As someone who really dislikes mathematical notation (pre-TLA+ proficiency), I think it's flawed.
You need to learn to think in math. Literally use math to solve CS problems.
This is fundamentally a different kind of thinking than writing code.
Once you learn to Think In Math™, the TLA+ notation is fine, even good—it maps 1:1 to your thoughts. Programming language notation would only get in the way.
The question of whether mathematics would become significantly more approachable if written not how it normally has been for the past hundred years but rather in programming language syntax, even though the symbols would not have the same meaning they do in programming, is not one I have the answer to. But even if TLA+ itself used programming syntax, because it would still be just maths and logic, once you'd want to learn something about a particular topic, the material would be in standard notation, so you'd still have to learn it.
And even if that weren't the case, and even if the mathematical notation were a serious obstacle, I think that obstacle is only significant in the first couple of days; after that, there are bigger challenges -- like getting used to describing things with maths -- that make the early syntax problem pretty negligible in comparison. There are other ways to specify discrete systems, but TLA+ chooses to do it with (pretty simple) mathematics. You have to know what you're getting into, namely learning how to use maths to specify. It isn't very hard compared to, say, learning how to program, but it is a challenge, albeit a fun and interesting one, that you have to want to tackle. But the payoff is quite big, in my opinion, even beyond being able to write specifications in TLA+ (which, in itself, has a big payoff in software quality compared to the effort required).
Those who've just started climbing a hill might complain about the first ten steps, because those are the ones they've taken. But the best way to get more people to the top isn't to flatten the first ten steps, but to show them why climbing the hill is worthwhile.
And yes, the syntax is weird. I understand it tries to mimic set theory notations (which I'm fine with), but transposing this in ascii didn't feel right.
I don't use TLA+ yet, I'd like to learn, but I've followed a lot of discussions on HN regarding this.
The other reason I don’t use it is that it’s very hard to inspect what you’re running. You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. It makes it really hard to convince yourself (and your peers) you haven’t assumed all of the state away.
After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.
You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818
But there often are easier ways to do sanity checks to "convince yourself you haven’t assumed all of the state away," usually either by asserting something believed to be false or by intentionally introducing an error in the spec, and letting TLC find a counterexample.
A mistake that could be automatically checked is specifying a system that is equivalent to FALSE (and so implies anything). I hope TLC adds a feature that allows you to check if your system implies FALSE. In the meantime, checking the invariant ¬Init has the same effect.
This detailed 4-part series by user "pron" is far more comprehensive to understand and start with TLA+: https://pron.github.io/posts/tlaplus_part1
The issue is that much real world software is not written in these languages (or Haskell)
Typescript and python are a lot more interesting.
https://adsharma.github.io/pysmt/
The proposal is to have a programming language and a specification language both with a pythonic syntax living in one file.
Coupled with a transpiler, it could make a capable system vs the C++/TLA+ based alternative.
I am a big fan of property based testing that can fuzz through very similar types of problems but it's not quite the same.
Or is tla+ just the thing to use and it's worth ploughing through?
I hated the syntax at first, and frankly, it took two weeks and about 500 pages of reading before it clicked (as to how to solve practical problems with it).
It's been a pleasure to use ever since. What is does you can't get from any other tool or methodology (with the same amount of effort).
> Are there good alternatives for solving the same / similar kinds of problems?
Not that I've found. It's really worth it to just learn TLA+.
There are quite a few alternatives. Alloy is pretty approachable and aims for the same or a similar space. I liked Event-B (based on B-Method), its tooling was nice. Z Notation (pronounced Zed) was my first examination of formal specifications, it lacked a lot of tooling for automation but I found it helped to clarify my reasoning about systems quite a bit. I wish I'd used it more, it's now a fuzzy memory for me.
That said, I like TLA+ specifically for what it's aimed at, modeling concurrent and distributed systems. It's very effective for this if you can take the time to understand it.
Most people who use TLA+ also seem to fire up Alloy once and awhile…
This issue alone is enough to dissuade me from using tla.
All software quality tools are imperfect, and even in the very few special cases where software can be realistically verified end-to-end, the behaviour of the actual system -- which also depends on hardware that can never be fully assured -- is not guaranteed.
The only question that matters when evaluating a software quality tool is: does it improve the software's quality for a cost that is lower than achieving the same improvement by other means? In other words, does it save us money and/or pain? For TLA+, the answer in many cases is absolutely yes. I.e. there is no better/cheaper/easier way to gain the same benefit.