That's interesting, are there more examples of such languages?

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

wow, that feels extremely more approachable.

Are there downsides to using that?

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.