TLA+ has its own quirks, you could add sugar here and there, but from semantic standpoint you couldn't do much. It's "unreadable" because requires some mental model most of developers don't have. My point: you either provide "simple" tools which could do nothing for real models or they become on same level of "unreadableness" really fast.
I taught a lot of people TLA+ and while there's definitely essential complexity, a nontrivial amount is just syntactic friction. Consider
\A x \in set: x.id /= 1 /\ ~x.active
all x in set: x.id != 1 && !x.active
That is literally what is holding me back every single time I get back to TLA+. I love your book and posts and always use it as reference to get back into it, but most of that "getting back" is just trying to remember all the minutia of the syntax. I wish there was simply a transpiler from some common syntax into TLA+. I don't even need Pluscal for the most part, and I'm fine with the concepts of temporal logic.
I agree, latexisms in TLA are on eye brow level of weirdness. Lesser punctuation syntax is always better.
It is in deed tricky, but we tried. We fully kept the semantics of TLA+, so the same mental model people still need to learn (at least a little), but a syntax that is much more familiar to engineers/programmers.
This is Quint [1], a different syntax for TLA+ with some extra tooling (type checker, CLI, evaluator, REPL, VSCode extension, testing framework, etc) which can be transpiled to TLA+ (which is a very direct translation, as the semantics is the same [2]) and therefore make use of the TLA+ tools as well (mainly the model checkers).
I think this is far from the same level of "unreadableness" than TLA+, and it makes formal methods much more approachable. It would be great if you could take a look and tell me whether you agree.
[1]: https://quint-lang.org/ [2]: https://quint-lang.org/docs/lang
I did an eval of Quint about year ago and did not find it compelling. It constantly refers to TLA+ and doesn't bring much benefits except typing. Syntax tries to cover underlying fact that state machine is expressed in terms of logic and math using "understandable" for programmers concept but it's very leaky in the end. IMHO "assign" is quite hard to grok without TLA experience. Documentation is scarce.
The most frustrating part it's hard to use with TLA+ background. I know how to do something in TLA but have no clue with Quint because translation rules aren't direct and obvious.
On the other hand it's a way better than PlusCal!
But I'm heavily biased. Please take this "critique" as a mumble from TLA+ initiated duckling.