Which is why you had to talk about TLC, not TLA+. And yeah, while the presence of printf-style debugging for specifications being model checked by TLC is technically executable-ish, I think in this case, it kind of proves the point that TLA+ itself isn't.

Regardless, I like the direction Quint is taking though I would quibble with this language in your reply:

> our tooling to find and diagnose typing errors [runs] prior to [...] any type checker

If you are diagnosing typing errors, then definitionally, you are running a type checker. It's great that it's fast and interactive, runs prior to the model checker, is easy for programmers to read/write, et cetera. But…it's still a type checker. :-)

Anyway, keep up the great work! I've been on your newsletter for a long time and love the work you guys are doing.