I agree with a lot of that, but in practice some syntactic sugar around types in TLA+ (or at least canned type invariant macros) would make it easier to write concise readable specs. Think "x is a natural number", "y is a member of set x", etc. It wouldn't satisfy the type theory folks, but would be nice for TLA+ users. In practice, it seems like everybody (including me) ends up re-writing a whole lot of type invariants in each TLA+ spec, and it would be nice to avoid that both to reduce boilerplate and to communicate to the reader what the author's intent was around data types.

It may be worthwhile to allow declarations of the form

    VARIABLE x ∈ Nat

but I haven't considered all the implications of doing that. May be worth a discussion on the mailing list or at the conference in September.

As to "satisfying the type theory folks," I'm not sure what it means. Type theory studies the features of typed formalisms; it makes no claims as to when working in a typed formalism is preferable to working in untyped ones (although different people have different opinions). There are implementations of TLA in typed formalisms (in particular, Isabelle and Coq). Lamport explains why he designed TLA+ as an untyped language.

I think it is worth a discussion.

I simply meant that adding simple macros wouldn't make TLA+ typed, and so wouldn't make the people who think TLA+ should be typed any happier than they are today.

There are typed TLA formalisms[1], but they're not called TLA+. I don't know what it means to want TLA+ to be typed. It's like saying someone wants the untyped lambda calculus to be typed. I can understand someone who thinks Lamport was misguided in designing TLA+ as an untyped formalism, but so far it seems that he was right (for the reasons I detailed in my Reddit comment).

[1]: https://www.isa-afp.org/entries/TLA.html, https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...