6 ms·

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 peop

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...
- xcfvbnkhnkjq 5y ago
  Having studied TLA+ a little bit, I'm curious - is there something flawed in the parent comment's argument?
  - pron 5y ago
    I would say that TLA+'s syntax is quite standard, or even conservative, similar to that of most maths language, and so quite the opposite from weird. 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.
  - erichocean 5y ago
    > is there something flawed in the parent comment's argument? 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.
yodsanklai 5y ago
To me, a big turn off was the Eclipse based interface. I would have been happy with minimal support (syntax highlighting, automatic formatting) for common editors and some command line tools. Maybe these things exist now, but last time I tried using the tool, this wasn't available out of the box. 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.
- erichocean 5y ago
  I use the Visual Studio Code TLA+ plugin, it's significantly nicer to work with.
skyde 5y ago
Did you try pluscal? My understanding is TLA+ is intended to be low level ( closer to theorem prover like z3) instead of a high level spec language.

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...

xcfvbnkhnkjq 5y ago
Having studied TLA+ a little bit, I'm curious - is there something flawed in the parent comment's argument?
- pron 5y ago
  I would say that TLA+'s syntax is quite standard, or even conservative, similar to that of most maths language, and so quite the opposite from weird. 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.
- erichocean 5y ago
  > is there something flawed in the parent comment's argument? 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.

yodsanklai 5y ago

To me, a big turn off was the Eclipse based interface. I would have been happy with minimal support (syntax highlighting, automatic formatting) for common editors and some command line tools. Maybe these things exist now, but last time I tried using the tool, this wasn't available out of the box. 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.

erichocean 5y ago
I use the Visual Studio Code TLA+ plugin, it's significantly nicer to work with.

skyde 5y ago

Did you try pluscal? My understanding is TLA+ is intended to be low level ( closer to theorem prover like z3) instead of a high level spec language.