[HN Gopher] Quint: A specification language based on the tempora...
___________________________________________________________________
Quint: A specification language based on the temporal logic of
actions (TLA)
I am on the dev team for this project and would be happy to answer
any questions and/or take note of any critical feedback :) Here's
a bit more detail: Quint is a modern, executable specification
language that is a particularly good fit for distributed systems,
such as blockchain protocols, distributed databases, and p2p
protocols. Quint combines the robust theoretical basis of the
Temporal Logic of Actions (TLA) with state-of-the-art static
analysis and development tooling.
Author : abathologist
Score : 88 points
Date : 2023-12-19 11:19 UTC (1 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| metaketa wrote:
| Recommended introduction talk for context:
|
| https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=Gatew...
|
| TLDR: compileable modeling language to model the high-level
| protocol of your blockchain (or any distributed system). It's a
| "digitalization" step of plain written English protocol
| specifications to code.
| just_mc wrote:
| This looks really nice. It's the first thing I have seen that
| appears to be approachable from a developer's perspective.
| abathologist wrote:
| That is our aim! If you give it a shot and find things that
| aren't so approachable, we'd live to hear how we can improve.
| crabbone wrote:
| One thing that was a demotivating factor (for me) about TLA+ is
| the syntax (I later realized that there's a more high-level
| language that looks more like a programming language and less
| like markup: PlusCal, but it was too late :). This looks a lot
| nicer.
| pron wrote:
| The syntax is needed so that simple mathematical substitutions
| and deductions could be applied. PlusCal is not "higher level",
| it's just similar to a programming language. In fact, TLA+
| makes it easy to write higher level specifications, i.e. those
| that go into less detail. One of the nice things you can do is
| write a smaller, high-level spec in TLA+ (e.g. you can specify
| "a program that sorts integer arrays in O(n^2)") and then a
| lower level spec, closer to code, in PlusCal, and tie the two
| together, showing that the latter is an implementation of the
| former.
|
| The simple mathematical syntax (and semantics [1]) of TLA+ has
| the advantage of making mathematical reasoning easier and it's
| more expressive; if it were like a programming language there
| would be too many things that TLA+ users would want to do but
| couldn't, certainly not as easily. Programming-language-like
| syntax and semantics has the advantage of being more familiar
| to programmers (many of which just want to run a model checker,
| and aren't interested in a more mathematical analysis of the
| specification (which actually makes specification easier, but
| only after gaining some experience). The two kinds of languages
| make different kinds of things either easier or harder.
|
| Overall, being programming-like helps programmers who just want
| model checking and then maybe to start dipping their toes into
| specification.
|
| ----
|
| [1]: What's more challenging for programmers is less the syntax
| and more the semantics. For example, the following function
| definition in TLA+ (using ASCII syntax) happens to _look_ a lot
| like programming in this particular case: f[x
| \in Int] == -f[x]
|
| it _looks_ like a programming subroutine that recursively calls
| itself ad-infinitum, but obviously, as in mathematics, it
| simply defines a function of the integers that is zero
| everywhere as that is the only definition that satisfies the
| equation and allows simple mathematical substitution.
|
| Another example could be (again, using the ASCII syntax):
| Inc(x) == x + 1
|
| which seems like an increment operator, but 3
| = Inc(x)'
|
| means something close to: "the system assigns 2 to x (or maybe
| something that's not a number)". In TLA+ things don't work like
| in programming -- they work like in maths -- and they must not
| work like in programming if you want to do things like high
| level specifications, refinements and more. The syntax tries to
| help and make that clear by trying to resemble maths rather
| than programming so that you wouldn't confuse the different
| meaning similar expressions have in these different domains.
| For those who do want to learn TLA+ (which is a language that's
| significantly simpler than Python but is not a programming
| language) is to forget any relationship it may have to
| programming and remember that even things that _look_ similar
| to programming work in a very different way. I would say that
| the relationship between TLA+ and programming is similar to
| that between the formula h = 0.5gt^2 and someone dropping a
| golf ball off a cliff in California.
|
| Those who aren't interested may still benefit from languages
| that are programming-like and offer model-checking. That's
| great, too!
| Taikonerd wrote:
| I thought I read one time that Leslie Lamport didn't _want_
| TLA+ to look like a programming language, because it might
| confuse developers into thinking it IS a programming language.
|
| I understand his logic, but at the same time, TLA+'s weird
| surface syntax put off a lot of people who otherwise could have
| used it. And PlusCal seemed like a halfway measure: more like a
| programming language, but still kinda... weird.
|
| So, I welcome Quint. And it's great that they seem interested
| in making the tooling fit with the normal developer ecosystem,
| such as LSP support.
| abathologist wrote:
| I can sympathize! We are aiming to maintain _most_ of the
| expressive power of TLA+ -- ideally everything you need for a
| concise, high-high level specification, that can be simulated
| and /or verified -- but with surface syntax that is more
| approachable coming from a programming background. If you're
| interested in seeing how it maps to TLA+, you can find much of
| that in this document:
| https://github.com/informalsystems/quint/blob/main/doc/lang....
|
| We still have lots of ways to improve, and -- we think -- lots
| of opportunities to improve our interop and complementary
| qualities in relation to TLA+ and TLC. But we have found the
| tools in their current state useful enough to be worth sharing
| :)
| asimpletune wrote:
| I'm trying to understand what is the difference between this and
| using TLA.
|
| For example, what is the difference between "robust theoretical
| basis of the Temporal Logic of Actions (TLA)" and "state-of-the-
| art static analysis"?
|
| Sorry, I'm not an expert in TLA, but I thought that static
| analysis was basically what it was used for.
| jleahy wrote:
| At very least it looks like it can do what TLA can do whilst
| being dramatically less painful to learn / work with. That is
| very much enough to be interesting.
| bugarela wrote:
| 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 wrote:
| > 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 wrote:
| > 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 wrote:
| > _(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
| abathologist wrote:
| 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/o
| rg....
|
| 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 wrote:
| > _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.
| bugarela wrote:
| I think they meant "model checker" instead of "type
| checker" in that sentence. Otherwise, of course, we need
| to run the type checker to get the type diagnosis.
| pron wrote:
| > 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.
| abathologist wrote:
| Those are great questions! Let me add a one addendum to
| bugarela's excellent explanation, to help disambiguate these
| three formalism:
|
| 1. TLA[0] is a logical calculus invented by Leslie Lamport.
|
| 2. TLA+[1] is a formal specification language, also invented by
| Leslie Lamport, with semantics based on and reducible to TLA.
|
| 3. quint is also a formal specification language with semantics
| based on and reducible to TLA.
|
| TLA+ can be understood as TLA extended with syntax sugar to
| help describe systems. On top of the logical calculus it adds
| niceties like `LET` bindings, syntax to represent common data
| structures, `CASE` expressions, a module system, etc. But TLA+
| also exposes the underlying logic directly, making the language
| extremely expressive. The flip side is that nonsensical
| formulas which may not be checkable are pretty easy to write.
|
| quint is a (programmer friendly) syntax that, while also
| desugaring to TLA, gives up expressivity to add the guardrails
| that we've found most helpful when specifying the systems we
| work on.
|
| Please let us know if you have any followup questions :)
|
| ---
|
| [0]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions
| [1]: https://en.wikipedia.org/wiki/TLA%2B
| Kevin09210 wrote:
| Clojure to TLA+
|
| https://github.com/Viasat/salt
|
| Successor: https://github.com/Viasat/halite
| bugarela wrote:
| I didn't take a very deep look yet, but this might be similar
| to https://github.com/pfeodrippe/recife
| zubairq wrote:
| Interesting
| Nevermark wrote:
| > We have covered all the aspects of our "Hello, world!" example.
| Actually, we could have written a much shorter example, but it
| would not demonstrate the distinctive features of Quint.
|
| Ouch! When I am trying to wrap my head around a new tool, I want
| a series of examples starting with _the absolute simplest
| possible example_.
|
| If I can see only one new concept demonstrated at a time, each in
| the simplest context possible, I can quickly develop a clear
| understanding. By quickly, I mean a solid understanding in
| minutes.
|
| Anything else just generates questions (and am I even thinking
| the right questions?) at a faster rate than lightbulbs.
| abathologist wrote:
| This is great feedback, thanks! Probably the first step
| tutorial should just be on something very straightforward, like
| an hour clock or a counter. I'll file an issue to introduce
| something more focused.
|
| Thanks again :)
|
| edit: https://github.com/informalsystems/quint/issues/1319
| nextaccountic wrote:
| How do you compare this with Alloy?
| bugarela wrote:
| I haven't really used Alloy before to give you a nice
| comparison, but some people have talked about differences in
| similarities between Alloy and TLA+ (i.e. in
| https://alloytools.discourse.group/t/alloy-6-vs-tla/329/13),
| and, in general, this should apply to Alloy vs Quint, since
| Quint is heavily based on TLA+. Evidently, the points regarding
| tooling and surface syntax won't really apply, as those are
| things Quint does not take from TLA+.
___________________________________________________________________
(page generated 2023-12-20 23:01 UTC)