4 ms·

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.
- rramadass 5y ago
  Well put! I was in the same boat i.e. wanting everything to be expressible in C/C++ type of syntax before i realized that it was quite the wrong way of looking at things and in particular; Mathematics. Mathematical Notation is fundamental while Programming Language Notation is incidental when looking at Mathematical subjects. It was merely an unwillingness to put forth effort to learn a new "shorthand conceptual language" that was holding me back. Once i learnt to read the notation and familiarized myself with it, things became much "easier and obvious".

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.

rramadass 5y ago
Well put! I was in the same boat i.e. wanting everything to be expressible in C/C++ type of syntax before i realized that it was quite the wrong way of looking at things and in particular; Mathematics. Mathematical Notation is fundamental while Programming Language Notation is incidental when looking at Mathematical subjects. It was merely an unwillingness to put forth effort to learn a new "shorthand conceptual language" that was holding me back. Once i learnt to read the notation and familiarized myself with it, things became much "easier and obvious".