6 ms·

Quint: A specification language based on the temporal logic of actions (TLA)

110 points by abathologist 3y ago

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.

deleted 3y ago
[deleted]
metaketa 3y ago
Recommended introduction talk for context: https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=GatewaytoCosmos 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 3y ago
This looks really nice. It's the first thing I have seen that appears to be approachable from a developer's perspective.
- abathologist 3y ago
  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 3y ago
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 3y ago
  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!
asimpletune 3y ago
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 3y ago
  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 3y ago
  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.
Kevin09210 3y ago
Clojure to TLA+ https://github.com/Viasat/salt https://github.com/Viasat/salt Successor: https://github.com/Viasat/halite https://github.com/Viasat/halite
- bugarela 3y ago
  I didn't take a very deep look yet, but this might be similar to https://github.com/pfeodrippe/recife https://github.com/pfeodrippe/recife
zubairq 3y ago
Interesting
Nevermark 3y ago
> 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 3y ago
  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 https://github.com/informalsystems/quint/issues/1319
  - deleted 3y ago
    [deleted]
nextaccountic 3y ago
How do you compare this with Alloy?
- bugarela 3y ago
  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 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+.
cyanydeez 3y ago
this sounds like something you'd plug into an LLM asA AGI
enigmassive 3y ago
This is something I really wanted to build when I learned about TLA+ over a year ago. Taking the core idea into a modern language and toolings. Congratulations that you actually did it!

110 points by abathologist 3y ago

deleted 3y ago

[deleted]

metaketa 3y ago

Recommended introduction talk for context: https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=GatewaytoCosmos 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 3y ago

This looks really nice. It's the first thing I have seen that appears to be approachable from a developer's perspective.

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

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

asimpletune 3y ago

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

Kevin09210 3y ago

Clojure to TLA+ https://github.com/Viasat/salt https://github.com/Viasat/salt Successor: https://github.com/Viasat/halite https://github.com/Viasat/halite

bugarela 3y ago
I didn't take a very deep look yet, but this might be similar to https://github.com/pfeodrippe/recife https://github.com/pfeodrippe/recife

zubairq 3y ago

Interesting

Nevermark 3y ago

> 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 3y ago
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 https://github.com/informalsystems/quint/issues/1319
- deleted 3y ago
  [deleted]

nextaccountic 3y ago

How do you compare this with Alloy?

bugarela 3y ago
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 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+.

cyanydeez 3y ago

this sounds like something you'd plug into an LLM asA AGI

enigmassive 3y ago

This is something I really wanted to build when I learned about TLA+ over a year ago. Taking the core idea into a modern language and toolings. Congratulations that you actually did it!