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 t

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.