> TLA+ is missing is any notion of executing code Which is why you had to talk about TLC, not TLA+. And yeah, while the presence of printf-style debugging for

> TLA+ is missing is any notion of executing code 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.