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?

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.

So is it for programmers or is it for mathematicians?

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.