If you were to sample 100 TLA+ specifications, you would find 100 descriptions of software systems using mathematical formulas. Physicists don't use different m

If you were to sample 100 TLA+ specifications, you would find 100 descriptions of software systems using mathematical formulas. Physicists don't use different mathematical notation when they write an ODE for a spring or electrical current. Also, I don't understand what notation would be appropriate. Functions in Haskell are much more similar to functions in Java than they are to either operators or functions in TLA+. You could use Java or Haskell notation, but what you'd be using it for would still behave differently from either one, which would only be more confusing. Even when it comes to simple things like conjunction and disjunction, over the past 50 years, programming languages have used at least three different popular representations, while over the last 100 years, mathematics have used one. Why is picking one of the three superior for writing mathematics in TLA+ than picking the one? Also, you should know that specification languages based on programming languages were the norm before TLA+. TLA+ intentionally broke away from that to offer something different, because Lamport believed it is simpler. I agree, but if you don't, you can use the specification languages that preceded TLA+, like Isabelle and Coq. So you're going to the one language that tried to make things easier by changing things up and asking, why did you change things up? Despite all that, after a three-day workshop, programmers use TLA+ to specify large and complex software systems, something that those who learn the programming-language-based specification languages do not, so perhaps Lamport was right.