> As for tooling, first of all, Quint has type checking, which TLA+ doesn't.

I wouldn't put it quite like that. It's not that TLA+ doesn't "do type checking" because TLA+ is just a language for writing mathematical descriptions of things. It doesn't "do" anything (do the formulas of Newtonian mechanics do type-checking?). It's more precise to say that TLA+ is an untyped language. But the model checker does check something like "typing" in the sense of set membership. I.e. the invariant □(x ∈ Int), i.e. "x is always an integer", can be checked with a TLA+ model checker just like many other invariants.

Furthermore, a model checker is "static" in the sense that, just like a type-checker, it doesn't "run" a "program". It's easy to see that a model checker doesn't run anything if you consider that a model checker can prove the following "type" on the right hand side of the implication:

    x ∈ BOOLEAN ∧ □[x' = TRUE ∨ x' = FALSE]_x ⇒ □(x ∈ BOOLEAN)

It proves it nearly instantaneously, even though every "execution" of the "program" on the left of the implication is infinite in its duration and there is an uncountably infinite number of such "execution", so clearly nothing is "executed" and the check isn't dynamic. So a TLA+ model checker does do something that's analogous-ish to type-checking.

However, it is true that by type-checking we normally mean an automated deductive process, i.e. one that applies inference rules, rather than an automated exhaustive analysis of the semantic domain, which is how a model-checker works. And yes, there are implications to the different ways "type checking" is done, especially when it comes to the algorithmic complexity of the checker.

This is just another example where comparisons to programming are unhelpful when describing mathematics that don't "run"; it just is.

It may be best to say that a language like Quint is inspired by the TLA logic (the TLA part of TLA+) and is similar to a programming language, whereas TLA+ is something else altogether (that requires learning something that is very much not programming) and leave it at that.

I admit that explaining the difference between programming (or something that's programming-like) and specifying a system with mathematics to people who are less familiar with the latter is difficult. It's a little like trying to explain the notion of a physics formula to a catapult builder in ancient Greece. There's clearly a relationship between the two (and some physics formulas may certainly be helpful when designing a catapult and make the catapult builder a better catapult builder), but they're also completely different things operating in two different domains (a formula isn't something that can fire a projectile).