Lamport would argue that if you're debating typed vs. untyped PLs, you're already missing the point, as all programming languages are necessarily[1] at a level that's too low for system/algorithmic thinking, and if you're working in a language appropriate to thinking about algorithms/systems, then the considerations surrounding typing are quite different from those pertaining to PLs (TLA+ happens to be untyped, but it's not a PL by any means).
[1]: Due to the requirement that they be efficiently compiled/interpreted.
As I understand it, TLA may technically be untyped but that's simply because you are supposed to implement your own more granular type checking as part of your spec.
It's true that TLA+ doesn't rely on types to specify properties, but it's still untyped. You could implement similar arbitrary properties in any programming language as predicates.
[1]: Due to the requirement that they be efficiently compiled/interpreted.