6 ms·

TLA+ is hard to learn (2018)

94 points by azhenley 5y ago

sesuximo 5y ago
Tla also introduces a new type of bug: differences between your tla model and your program. And I found that in order to get tla to reason about large programs, you had to express the model in ways that look very different from the program. This issue alone is enough to dissuade me from using tla.
- mhh__ 5y ago
  But the whole purpose is to check your model before you write code, no? I get that differences are hard but it's better than nothing
- colanderman 5y ago
  I never recommend TLA for reasoning about programs, but about models. It's great for describing a system you're still designing.
  - rramadass 5y ago
    Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declarative logic used in specifications vs. say predicate transformers used in proving program correctness?
- pron 5y ago
  That's like saying that tests introduce a new kind of bug -- behaviours that aren't explored at all -- and that that serious issue (and it is, indeed, extremely serious) should dissuade you from writing and running tests. 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.
- wtetzner 5y ago
  The alternative is to not check the model at all. Doesn’t really seem better.
smallpipe 5y ago
The tool is also pretty abysmal at telling you why it can’t parse the thing you wrote. For me that was the reason #1 it’s hard to learn. 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.
- pron 5y ago
  > You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818 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.
  - smallpipe 5y ago
    I agree it’s workable, but it’s a bit of a hack. Commercial formal verification software for RTL has this built-in, and once you have 10+ people updating a spec, you need an automated way of checking for accidental constraints.
    - pron 5y ago
      I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. 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.
- thisiscorrect 5y ago
  TLA+ as a formal language for specifying systems is quite good. But the quasi-official toolchain for working with it [1] including TLC and the sanitizer are not well maintained. They were pretty resistant to outside contributions when I tried. I have hope that a better toolchain for working with the TLA+ language can come along. The underpinning language is well designed. Lamport is no slouch. [1] https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus
devnull3 5y ago
For me the big issue is the weird syntax. I know this may sound superficial but it is really off-putting. My guess is that if syntax is improved, a lot of people will give it a shot.
- asimpletune 5y ago
  I think I've seen on HN stuff built on TLA+ but with a typescript-like syntax. A lot of people argue though that by making it more programming-language-like, vs math-like, that you're trading better tools for the job in exchange for what's familiar. I don't use TLA+ yet, I'd like to learn, but I've followed a lot of discussions on HN regarding this.
- pron 5y ago
  TLA+'s syntax is pretty close to standard mathematical notation, and is very similar to other languages for writing mathematics, so it is actually quite mundane. Anything that's more programming-like would have made it weird compared to most other mathematics languages. 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_example_that_tla_is_math_not/ https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...
smitty1e 5y ago
TLA = Three-Letter Acronym?
- mhh__ 5y ago
  What's the top result if you Google "TLA+"?
  - 6gvONxR4sf7o 5y ago
    Or click the article.
    - smitty1e 5y ago
      Did.
- wtetzner 5y ago
  Temporal Logic of Actions
IanCal 5y ago
Are there good alternatives for solving the same / similar kinds of problems? 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?
- erichocean 5y ago
  It's worth plowing 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+.
  - raegis 5y ago
    Yup, I agree strongly. I watched the Lamport videos when on paternity leave, and really enjoyed it. The main benefit for me was that writing a spec in TLA+ allows me to "get my mind right" before writing programs. I was in love with the notation from the beginning (but I was a math major in school so I'm biased).
- Jtsummers 5y ago
  https://en.wikipedia.org/wiki/Specification_language https://en.wikipedia.org/wiki/Specification_language 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.
  - erichocean 5y ago
danidiaz 5y ago
"Spectacle" is a Haskell DSL for writing TLA+ specifications: https://awakesecurity.com/blog/spectacle-a-language-for-writing-and-checking-formal-specifications-in-haskell/ https://awakesecurity.com/blog/spectacle-a-language-for-writ...
- hwayne 5y ago
  It's inspired by TLA+, but it uses a different semantics, I think.
michaelt 5y ago
TLA+ can be a powerful tool in certain situations - but it's got some... unique ways of doing things. 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.
- pron 5y ago
  All of TLA+ (except the proof language), how all the symbols are typed, and all of the standard modules can be found on this cheatsheet: https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf 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.
adsharma 5y ago
Z3-solver is a popular backend for specifying properties about programs. Dafny, Viper, Boogie are all systems built on top of it. 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/ 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.
rramadass 5y ago
The blog post is too vague and not really helpful. 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 https://pron.github.io/posts/tlaplus_part1

94 points by azhenley 5y ago

Tla also introduces a new type of bug: differences between your tla model and your program. And I found that in order to get tla to reason about large programs, you had to express the model in ways that look very different from the program. This issue alone is enough to dissuade me from using tla.

mhh__ 5y ago
But the whole purpose is to check your model before you write code, no? I get that differences are hard but it's better than nothing
colanderman 5y ago
I never recommend TLA for reasoning about programs, but about models. It's great for describing a system you're still designing.
- rramadass 5y ago
  Elaborate please; Without reasoning about programs how do you come up with the predicates which constitute a Model? Are you making a distinction between declarative logic used in specifications vs. say predicate transformers used in proving program correctness?
pron 5y ago
That's like saying that tests introduce a new kind of bug -- behaviours that aren't explored at all -- and that that serious issue (and it is, indeed, extremely serious) should dissuade you from writing and running tests. 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.
wtetzner 5y ago
The alternative is to not check the model at all. Doesn’t really seem better.

smallpipe 5y ago

The tool is also pretty abysmal at telling you why it can’t parse the thing you wrote. For me that was the reason #1 it’s hard to learn. 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.

pron 5y ago
> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818 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.
- smallpipe 5y ago
  I agree it’s workable, but it’s a bit of a hack. Commercial formal verification software for RTL has this built-in, and once you have 10+ people updating a spec, you need an automated way of checking for accidental constraints.
  - pron 5y ago
    I don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. 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.
thisiscorrect 5y ago
TLA+ as a formal language for specifying systems is quite good. But the quasi-official toolchain for working with it [1] including TLC and the sanitizer are not well maintained. They were pretty resistant to outside contributions when I tried. I have hope that a better toolchain for working with the TLA+ language can come along. The underpinning language is well designed. Lamport is no slouch. [1] https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus

devnull3 5y ago

For me the big issue is the weird syntax. I know this may sound superficial but it is really off-putting. My guess is that if syntax is improved, a lot of people will give it a shot.

asimpletune 5y ago
I think I've seen on HN stuff built on TLA+ but with a typescript-like syntax. A lot of people argue though that by making it more programming-language-like, vs math-like, that you're trading better tools for the job in exchange for what's familiar. I don't use TLA+ yet, I'd like to learn, but I've followed a lot of discussions on HN regarding this.
pron 5y ago
TLA+'s syntax is pretty close to standard mathematical notation, and is very similar to other languages for writing mathematics, so it is actually quite mundane. Anything that's more programming-like would have made it weird compared to most other mathematics languages. 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_example_that_tla_is_math_not/ https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...

smitty1e 5y ago

TLA = Three-Letter Acronym?

mhh__ 5y ago
What's the top result if you Google "TLA+"?
- 6gvONxR4sf7o 5y ago
  Or click the article.
  - smitty1e 5y ago
    Did.
wtetzner 5y ago
Temporal Logic of Actions

IanCal 5y ago

Are there good alternatives for solving the same / similar kinds of problems? 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?

erichocean 5y ago
It's worth plowing 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+.
- raegis 5y ago
  Yup, I agree strongly. I watched the Lamport videos when on paternity leave, and really enjoyed it. The main benefit for me was that writing a spec in TLA+ allows me to "get my mind right" before writing programs. I was in love with the notation from the beginning (but I was a math major in school so I'm biased).
Jtsummers 5y ago
https://en.wikipedia.org/wiki/Specification_language https://en.wikipedia.org/wiki/Specification_language 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.
- erichocean 5y ago

danidiaz 5y ago

"Spectacle" is a Haskell DSL for writing TLA+ specifications: https://awakesecurity.com/blog/spectacle-a-language-for-writing-and-checking-formal-specifications-in-haskell/ https://awakesecurity.com/blog/spectacle-a-language-for-writ...

hwayne 5y ago
It's inspired by TLA+, but it uses a different semantics, I think.

michaelt 5y ago

TLA+ can be a powerful tool in certain situations - but it's got some... unique ways of doing things. 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.

pron 5y ago
All of TLA+ (except the proof language), how all the symbols are typed, and all of the standard modules can be found on this cheatsheet: https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf 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.

adsharma 5y ago

Z3-solver is a popular backend for specifying properties about programs. Dafny, Viper, Boogie are all systems built on top of it. 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/ 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.

rramadass 5y ago

The blog post is too vague and not really helpful. 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 https://pron.github.io/posts/tlaplus_part1