4 ms·

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 b

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 :-)
pron 5y ago
I agree with better debugability (there's now a TLA+ debugger) and better error messages, but I think that programming syntax would only make things easier on the first few days, and actually make things harder later: for one, you'd still need to learn mathematical notation because all the relevant material anywhere on logic uses it, and because the meaning of the syntax would still be very different from programming. > 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.

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 :-)

pron 5y ago

I agree with better debugability (there's now a TLA+ debugger) and better error messages, but I think that programming syntax would only make things easier on the first few days, and actually make things harder later: for one, you'd still need to learn mathematical notation because all the relevant material anywhere on logic uses it, and because the meaning of the syntax would still be very different from programming. > 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.