I would say that TLA+'s syntax is quite standard, or even conservative, similar to that of most maths language, and so quite the opposite from weird. The quest

I would say that TLA+'s syntax is quite standard, or even conservative, similar to that of most maths language, and so quite the opposite from weird. The question of whether mathematics would become significantly more approachable if written not how it normally has been for the past hundred years but rather in programming language syntax, even though the symbols would not have the same meaning they do in programming, is not one I have the answer to. But even if TLA+ itself used programming syntax, because it would still be just maths and logic, once you'd want to learn something about a particular topic, the material would be in standard notation, so you'd still have to learn it. And even if that weren't the case, and even if the mathematical notation were a serious obstacle, I think that obstacle is only significant in the first couple of days; after that, there are bigger challenges -- like getting used to describing things with maths -- that make the early syntax problem pretty negligible in comparison. There are other ways to specify discrete systems, but TLA+ chooses to do it with (pretty simple) mathematics. You have to know what you're getting into, namely learning how to use maths to specify. It isn't very hard compared to, say, learning how to program, but it is a challenge, albeit a fun and interesting one, that you have to want to tackle. But the payoff is quite big, in my opinion, even beyond being able to write specifications in TLA+ (which, in itself, has a big payoff in software quality compared to the effort required). Those who've just started climbing a hill might complain about the first ten steps, because those are the ones they've taken. But the best way to get more people to the top isn't to flatten the first ten steps, but to show them why climbing the hill is worthwhile.