3 ms·

I think your judgment is clouded by this insistence that you're doing math rather than something which is squarely in the middle of the cs/math venn diagram. Re

I think your judgment is clouded by this insistence that you're doing math rather than something which is squarely in the middle of the cs/math venn diagram. Relational algebra has an accepted notation for left outer-join (⟕). Do you think `I><|` is preferable to `LEFT JOIN` because mathematics™? If I were to sample 100 TLA+ specifications, do you think I would find more people specifying things like paxos and concurrency models, or would I find people doing algebraic geometry and number theory?

pron 6y ago
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.

pron 6y ago

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.