5 ms·

Hey! We just changed the description (yesterday) to avoid this confusion - sorry! By static analysis there we actually mean things like type and effect checking

Hey! We just changed the description (yesterday) to avoid this confusion - sorry! By static analysis there we actually mean things like type and effect checking. With either a TLA+ spec or a Quint spec, you can run a model checker to verify properties or get counterexamples. That's the main similarity. As Quint is based on TLA+, we can atually use the same model checkers (that were originally implemented for TLA+). The main differences between TLA+ and Quint are the surface syntax and the tooling (beyond the model checker). While TLA+ has an indentation-based hard-to-parse mathematical syntax (that looks quite pretty in LaTeX), Quint has a typed programming language styled syntax and a very simple parser, making it easier to develop tools around it. As for tooling, first of all, Quint has type checking, which TLA+ doesn't. Our IDE support is also more similar to that of modern programming languages - with features like "Go to definition". With this, we hope (and have seen many reports of) programmers/engineers having an easier and better time writing Quint specs then they used to have with TLA+ tooling. Quint also has support for execution of specs with random simulation, a testing framework and a REPL. In contrast, TLA+ is a much more permissive language, and you can express more mathematical things that, for instance, could never be executed or are not even supported by TLA+ existing model checkers (TLC and Apalache). TLA+ has a proof system (TLAPS), which Quint does not. Quint imposes many restrictions with the goal of preventing people to write things they don't really understand - which are possible in TLA+. Those restrictions are useful, just as type and effect systems are useful. But mathematicians that really know what they are doing and need more powerful expressivity will likely prefer TLA+ over Quint. Quint is aimed at programmers and engineers. They are complementary, not direct competition.

pron 3y ago
> As for tooling, first of all, Quint has type checking, which TLA+ doesn't. I wouldn't put it quite like that. It's not that TLA+ doesn't "do type checking" because TLA+ is just a language for writing mathematical descriptions of things. It doesn't "do" anything (do the formulas of Newtonian mechanics do type-checking?). It's more precise to say that TLA+ is an untyped language. But the model checker does check something like "typing" in the sense of set membership. 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. Furthermore, a model checker is "static" in the sense that, just like a type-checker, it doesn't "run" a "program". It's easy to see that a model checker doesn't run anything if you consider that a model checker can prove the following "type" on the right hand side of the implication: x ∈ BOOLEAN ∧ □[x' = TRUE ∨ x' = FALSE]_x ⇒ □(x ∈ BOOLEAN) It proves it nearly instantaneously, even though every "execution" of the "program" on the left of the implication is infinite in its duration and there is an uncountably infinite number of such "execution", so clearly nothing is "executed" and the check isn't dynamic. So a TLA+ model checker does do something that's analogous-ish to type-checking. 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. This is just another example where comparisons to programming are unhelpful when describing mathematics that don't "run"; it just is. It may be best to say that a language like Quint is inspired by the TLA logic (the TLA part of TLA+) and is similar to a programming language, whereas TLA+ is something else altogether (that requires learning something that is very much not programming) and leave it at that. I admit that explaining the difference between programming (or something that's programming-like) and specifying a system with mathematics to people who are less familiar with the latter is difficult. It's a little like trying to explain the notion of a physics formula to a catapult builder in ancient Greece. There's clearly a relationship between the two (and some physics formulas may certainly be helpful when designing a catapult and make the catapult builder a better catapult builder), but they're also completely different things operating in two different domains (a formula isn't something that can fire a projectile).
- nextaccountic 3y ago
  > 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

pron 3y ago

> As for tooling, first of all, Quint has type checking, which TLA+ doesn't. I wouldn't put it quite like that. It's not that TLA+ doesn't "do type checking" because TLA+ is just a language for writing mathematical descriptions of things. It doesn't "do" anything (do the formulas of Newtonian mechanics do type-checking?). It's more precise to say that TLA+ is an untyped language. But the model checker does check something like "typing" in the sense of set membership. 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. Furthermore, a model checker is "static" in the sense that, just like a type-checker, it doesn't "run" a "program". It's easy to see that a model checker doesn't run anything if you consider that a model checker can prove the following "type" on the right hand side of the implication: x ∈ BOOLEAN ∧ □[x' = TRUE ∨ x' = FALSE]_x ⇒ □(x ∈ BOOLEAN) It proves it nearly instantaneously, even though every "execution" of the "program" on the left of the implication is infinite in its duration and there is an uncountably infinite number of such "execution", so clearly nothing is "executed" and the check isn't dynamic. So a TLA+ model checker does do something that's analogous-ish to type-checking. 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. This is just another example where comparisons to programming are unhelpful when describing mathematics that don't "run"; it just is. It may be best to say that a language like Quint is inspired by the TLA logic (the TLA part of TLA+) and is similar to a programming language, whereas TLA+ is something else altogether (that requires learning something that is very much not programming) and leave it at that. I admit that explaining the difference between programming (or something that's programming-like) and specifying a system with mathematics to people who are less familiar with the latter is difficult. It's a little like trying to explain the notion of a physics formula to a catapult builder in ancient Greece. There's clearly a relationship between the two (and some physics formulas may certainly be helpful when designing a catapult and make the catapult builder a better catapult builder), but they're also completely different things operating in two different domains (a formula isn't something that can fire a projectile).

nextaccountic 3y ago
> 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