TLA+ Action Properties

The other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo

I haven't used salt, but the thing to understand is that even when the syntax used is Clojure, the semantics is TLA+'s. So, for example, if you use a Clojure function syntax to define a TLA+ operator, that will not behave like a Clojure function, but like a TLA+ operator, which behaves very differently from Clojure functions. So the symbols on the screen might be more familiar, but their meaning will be different from their meaning in Clojure. I think that is more confusing, which would be a downside, but if you find that more approachable -- great, use that.

I've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.

The syntax isn't for everyone and the tooling has some issues.

It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific operator; I think writing maths in a less familiar notation would be less appealing and require more training [2]. I did say that the tooling is missing an HTML formatter, which is why some bloggers prefer posting the source rather than the typeset maths. Still, the syntax -- standard mathematical notation -- isn't for everyone, just as Python or Java syntax isn't for everyone, either, and yeah, the tooling has some issues.

Also, yes, it is my opinion that if you focus on an editing environment -- which I like, BTW -- for short mathematical texts that you rarely actually edit compared to most other kinds of texts, then you're missing something quite fundamental about TLA+ (if you don't like the editor, pen and paper is another nice editing environment for TLA+; it's also a standard maths editing environment, but it feels more than 20 years old).

But that's just my opinion, and you don't have to agree with it one bit, just as I don't have to agree with yours. I'm not the boss of TLA+, nor its official ambassador, just someone who likes it, and you should form your own opinions. You really shouldn't take what anyone else you don't personally know says on the internet too seriously. I do like TLA+ a lot, which is why I'm exited to talk about it, but if you like it for completely different reasons or even don't like it at all, that's perfectly fine, too. My enjoyment of TLA+ or practical gain from it isn't harmed by you not liking it. It is fun to talk about something you like with others who like it, too, but if we all liked the same things the world would be pretty boring. Many people dislike the things I like, and sometimes I even like arguing with them. But it's not my mission to get you to like the same things I do.

[1]: That notation is due to https://en.wikipedia.org/wiki/C._I._Lewis#Logic

[2]: E.g. TLA+ functions don't behave like programming language subroutines; using the same syntax might be more familiar, but also more confusing because the text would look the same but mean something different.

Do you know TLA+? You sound like you've totally missed the point.

I agree it's a barrier for beginners, but I think this is a good barrier, which makes the next, bigger ones, easier to overcome. A step is also a barrier, but I'd rather face more, lower steps than fewer taller ones. By the time you realise neither operators nor functions work at all like functions from programming, the syntax has helped to put your mind in a "this is not programming" mode. Also, || and && are almost universally used in programming languages today, but they weren't thirty years ago, and might not be thirty years from now (Zig doesn't use them and neither does Nim), and even in C, C++, and Rust they have similar but subtly different meaning than | and & involving evaluation, a concept that TLA+ doesn't have -- now there's a more interesting and more important unfamiliar TLA+ thing -- while ∨ and ∧ have been used much longer than that and aren't going anywhere. So every person might prefer something that's already familiar to them, but there is no alternative that's really universal. If you go to Wikipedia -- say, https://en.wikipedia.org/wiki/Logical_connective -- they use "TLA+ notation," not C notation.

Anyway, there are other, and more important, things in TLA+ that are much less familiar from programming (e.g. there's no evaluation) than how to write logical or, and still TLA+ has been more successful at teaching programmers to specify more complex systems more quickly than any other specification language I'm aware of.

It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+.

Anyway, it's not what you're supposed to read. The vast majority of TLA+ is readable to someone familiar with ordinary mathematical notation within two to ten minutes of training (if you know temporal logic, then almost all of TLA+ is readable within minutes). See e.g. this complete (and very sophisticated in its use of advanced TLA+) specification, written at Arm, of CPU speculation side-channels: http://www.procode.org/cachespec/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.