| > That's the same thing as not having static types. I didn't say it had static types. I was referring specifically to the notion of type checking. > dynamically typed languages are just untyped languages There are no dynamic types in TLA+ just as there aren't in the formula F = ma. There is nothing here that's running, and all the automated analysis, including of the sets that corresponds to types doesn't run anything. > That's just checking a dynamic typing property There is no "dynamism" here. The model checker checks that the "type" (really set membership) holds in any possible execution, each of which potentially infinite in duration, out of a countless infinity of executions. It's also a "static" check, it's just that it isn't syntactic. > Static types are static _by construction_, you don't need any dynamic information to type check them And neither do you need any "dynamic" information in TLA+. Dynamic types are a programming notion. TLA+ is not a programming language. |