2 ms·

> much of which is immediately familiar to anyone who reads maths Most programmers don't read math. A tool pitched to programmers gains no advantage from being

> much of which is immediately familiar to anyone who reads maths Most programmers don't read math. A tool pitched to programmers gains no advantage from being readable primarily by mathematicians.

pron 6y ago
But that tool is mathematics. As far as I know -- at least, that's what things were like in my time in school -- when programmers learn mathematics they use standard notation, not their own. When they use the tool called natural language to write documentation, they also use standard notation, not their own, and when they study diagrams they (at least I) prefer looking at a pictures with lines rather than SVG source. I don't understand why a tool that is used by programmers but is nothing at all like a computer program should use computer program notation, and I don't think programmers would prefer reading mathematics differently from everyone else. I believe the reason this comes up in the first place is that people confuse TLA+'s mathematics with programming (or else why would they even ask something so different from programming to look like programming?). There are specification languages that are, or look like, programming languages; TLA+ came later and is intentionally different -- what's different isn't just the notation but the very meaning of the expressions you write. Why is it different? Because mathematics is simpler than even the most basic programming language -- which has such complex notions like a call stack or evaluation order -- and therefore clearer, and clarity is of the utmost importance in specification. I grew to appreciate that a great deal, and I think that decision makes TLA+ both clearer and more powerful than other specification languages. But you are right -- familiarity to programmers isn't one of it's strengths, but it has many others that, in my opinion, more than make up for that.
- jacques_chester 6y ago
  So is it for programmers or is it for mathematicians?
  - pron 6y ago
    It is mathematics for anyone who wants to describe discrete and hybrid systems, including programmers. But I believe mathematics is used by mathematicians, physicists, engineers of many kinds, and biologists for many different things -- that's what mathematics is for -- and they all use pretty much the same notation. Also, and this is important, there is no standard programming notation for mathematics. TLA+ operators and functions simply don't behave like subroutines in any programming language. I think using the same symbols, but with a different meaning, would be more rather than less confusing. For example, when in TLA+ you specify the function, f, from the integers to the integers such that f(x) = -f(x), you've obviously defined the zero function; I'm not aware of any programming language that works like that. While TLA+ doesn't have macros, the value of x = 3 ∧ Foo(x) = 5 might not be equal to x = 3 ∧ Foo(3) = 5, and I'm not aware of any non-logic programming language that works like that, either, at least not without some hidden complexity (simple mathematics also doesn't work like that, but this is because TLA+ is a modal logic), and logic programming languages have syntax that isn't any more familiar to non-logic programming language programmers than TLA+'s.
- lakecresva 6y ago
  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.

> much of which is immediately familiar to anyone who reads maths Most programmers don't read math. A tool pitched to programmers gains no advantage from being readable primarily by mathematicians.

pron 6y ago

But that tool is mathematics. As far as I know -- at least, that's what things were like in my time in school -- when programmers learn mathematics they use standard notation, not their own. When they use the tool called natural language to write documentation, they also use standard notation, not their own, and when they study diagrams they (at least I) prefer looking at a pictures with lines rather than SVG source. I don't understand why a tool that is used by programmers but is nothing at all like a computer program should use computer program notation, and I don't think programmers would prefer reading mathematics differently from everyone else. I believe the reason this comes up in the first place is that people confuse TLA+'s mathematics with programming (or else why would they even ask something so different from programming to look like programming?). There are specification languages that are, or look like, programming languages; TLA+ came later and is intentionally different -- what's different isn't just the notation but the very meaning of the expressions you write. Why is it different? Because mathematics is simpler than even the most basic programming language -- which has such complex notions like a call stack or evaluation order -- and therefore clearer, and clarity is of the utmost importance in specification. I grew to appreciate that a great deal, and I think that decision makes TLA+ both clearer and more powerful than other specification languages. But you are right -- familiarity to programmers isn't one of it's strengths, but it has many others that, in my opinion, more than make up for that.

jacques_chester 6y ago
So is it for programmers or is it for mathematicians?
- pron 6y ago
  It is mathematics for anyone who wants to describe discrete and hybrid systems, including programmers. But I believe mathematics is used by mathematicians, physicists, engineers of many kinds, and biologists for many different things -- that's what mathematics is for -- and they all use pretty much the same notation. Also, and this is important, there is no standard programming notation for mathematics. TLA+ operators and functions simply don't behave like subroutines in any programming language. I think using the same symbols, but with a different meaning, would be more rather than less confusing. For example, when in TLA+ you specify the function, f, from the integers to the integers such that f(x) = -f(x), you've obviously defined the zero function; I'm not aware of any programming language that works like that. While TLA+ doesn't have macros, the value of x = 3 ∧ Foo(x) = 5 might not be equal to x = 3 ∧ Foo(3) = 5, and I'm not aware of any non-logic programming language that works like that, either, at least not without some hidden complexity (simple mathematics also doesn't work like that, but this is because TLA+ is a modal logic), and logic programming languages have syntax that isn't any more familiar to non-logic programming language programmers than TLA+'s.
lakecresva 6y ago
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.