3 ms·

> It's more precise to say that TLA+ is an untyped language. That's the same thing as not having static types. (From the POV of static types, dynamically typed

> It's more precise to say that TLA+ is an untyped language. That's the same thing as not having static types. (From the POV of static types, dynamically typed languages are just untyped languages, that is, languages that have exactly one type) > I.e. the invariant □(x ∈ Int), i.e. "x is always an integer", can be checked with a TLA+ model checker just like many other invariants. That's just checking a dynamic typing property (that is, something tha could in principle vary during the execution of the program, but you just proved that it doesn't). That is, this is checking that certain dynamic types stay the same. (which is totally okay, and it's true that if you restrict dynamic types enough you can show there's a statically typed program that is equivalent) > However, it is true that by type-checking we normally mean an automated deductive process, i.e. one that applies inference rules, rather than an automated exhaustive analysis of the semantic domain, which is how a model-checker works. And yes, there are implications to the different ways "type checking" is done, especially when it comes to the algorithmic complexity of the checker. Yep! Static types are static _by construction_, you don't need any dynamic information to type check them

erichocean 3y ago
> (From the POV of static types, dynamically typed languages are just untyped languages, that is, languages that have exactly one type) I believe the mistake you are making is assuming that TLA+ has some kind of runtime where things are "executed" (static vs. dynamic in the context of programming languages refers to, roughly, compile-time vs. execution-time). Model checking in TLA+ is actually analogous to "running a compiler", not running a REPL or whatever. It's definitely NOT a runtime. TLA+ has no "dynamic" aspect at all, it's all "static" from the POV of language theory. And since it DOES provide a way (read: syntax) to create and check types (as the GP shows) and those types are checked statically (again, remember: there is no execution happening here), TLA+ is formally (and practically) equivalent to a language that has a different syntactic way to specify types, i.e. one that programmers are more familiar with. What TLA+ is missing is any notion of executing code. That's what makes it a specification language and not an implementation language. Most programming languages are implementation languages, with a bit of "specification"—usually types—sprinkled on top. TLA+ is specification-only, no implementation stuff is written down. So to recap, from a language-theoretic POV, TLA+ absolutely supports "static typing" in the way that it is usually understood and used by programmers and language theoreticians, but with a syntax that is unfamiliar (because it is a specification language). For completeness, you can specify modern type inference algorithms like MLstruct/MLsub [0] in TLA+ and the model checker will happily apply them to your TLA+ specification (again, statically—at compile-time, which is really "model checking" time). [0] https://lptk.github.io/files/[v8.0]%20mlstruct.pdf https://lptk.github.io/files/[v8.0]%20mlstruct.pdf
- abathologist 3y ago
  I think you and Ron are confusing the relevant phase distinction the rest of us have in mind when we talk about type checking in this context. What we mean is that quint, the language, is expressed on top of a many-sorted logic which allows our tooling to find and diagnose typing errors prior to *running* any type checker. The TLA Toolbox doesn't support this, and TLA+, like TLA itself, is untyped. TLC can (and will) raise errors while in the process of checking your model due to the kinds of problems we usually call "typing errors". Quint and apalache shouldn't do this. I hope this helps clarify a bit. We understand that, viewed purely theoretically, TLA+ has no dynamic aspect at all, etc. However, our team is very focused on the fusion of theory and practice, and we think it's important to ground our understanding and our discourse in the way the specification languages are actually used by real people given the existing tools. While it may be true in theory that > What TLA+ is missing is any notion of executing code. The file `TLC.tla` in the `StandardModules` includes these lines: ``` Print(out, val) == val PrintT(out) == TRUE (* This expression equals TRUE, but evaluating it causes TLC to print *) (* the value of out. *) ``` https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla#L17-L22 https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.... In any case, our whole team thinks TLA is great, and we're happy people like you and Ron find it so useful and insightful. We also think it is a very insightful tool for guiding understanding :)
  - erichocean 3y ago
    > 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.
pron 3y ago
> 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.

erichocean 3y ago

> (From the POV of static types, dynamically typed languages are just untyped languages, that is, languages that have exactly one type) I believe the mistake you are making is assuming that TLA+ has some kind of runtime where things are "executed" (static vs. dynamic in the context of programming languages refers to, roughly, compile-time vs. execution-time). Model checking in TLA+ is actually analogous to "running a compiler", not running a REPL or whatever. It's definitely NOT a runtime. TLA+ has no "dynamic" aspect at all, it's all "static" from the POV of language theory. And since it DOES provide a way (read: syntax) to create and check types (as the GP shows) and those types are checked statically (again, remember: there is no execution happening here), TLA+ is formally (and practically) equivalent to a language that has a different syntactic way to specify types, i.e. one that programmers are more familiar with. What TLA+ is missing is any notion of executing code. That's what makes it a specification language and not an implementation language. Most programming languages are implementation languages, with a bit of "specification"—usually types—sprinkled on top. TLA+ is specification-only, no implementation stuff is written down. So to recap, from a language-theoretic POV, TLA+ absolutely supports "static typing" in the way that it is usually understood and used by programmers and language theoreticians, but with a syntax that is unfamiliar (because it is a specification language). For completeness, you can specify modern type inference algorithms like MLstruct/MLsub [0] in TLA+ and the model checker will happily apply them to your TLA+ specification (again, statically—at compile-time, which is really "model checking" time). [0] https://lptk.github.io/files/[v8.0]%20mlstruct.pdf https://lptk.github.io/files/[v8.0]%20mlstruct.pdf

abathologist 3y ago
I think you and Ron are confusing the relevant phase distinction the rest of us have in mind when we talk about type checking in this context. What we mean is that quint, the language, is expressed on top of a many-sorted logic which allows our tooling to find and diagnose typing errors prior to *running* any type checker. The TLA Toolbox doesn't support this, and TLA+, like TLA itself, is untyped. TLC can (and will) raise errors while in the process of checking your model due to the kinds of problems we usually call "typing errors". Quint and apalache shouldn't do this. I hope this helps clarify a bit. We understand that, viewed purely theoretically, TLA+ has no dynamic aspect at all, etc. However, our team is very focused on the fusion of theory and practice, and we think it's important to ground our understanding and our discourse in the way the specification languages are actually used by real people given the existing tools. While it may be true in theory that > What TLA+ is missing is any notion of executing code. The file `TLC.tla` in the `StandardModules` includes these lines: ``` Print(out, val) == val PrintT(out) == TRUE (* This expression equals TRUE, but evaluating it causes TLC to print *) (* the value of out. *) ``` https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla#L17-L22 https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.... In any case, our whole team thinks TLA is great, and we're happy people like you and Ron find it so useful and insightful. We also think it is a very insightful tool for guiding understanding :)
- erichocean 3y ago
  > 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.

pron 3y ago

> 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.