5 ms·

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

by 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.
  - 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".
devnull3 5y ago
I see the point you are making. 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/ 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/ 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 https://reference.wolfram.com/language/ref/ForAll.html
- rramadass 5y ago
  As a Software Person who is self-studying Formal Methods and TLA+ i can categorically state that you are wrong! 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 :-)

by pron 5y ago

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

devnull3 5y ago

I see the point you are making. 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/ 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/ 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 https://reference.wolfram.com/language/ref/ForAll.html

rramadass 5y ago
As a Software Person who is self-studying Formal Methods and TLA+ i can categorically state that you are wrong! 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 :-)