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.
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.
Thanks again :)
edit: https://github.com/informalsystems/quint/issues/1319
Deleted Comment
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.
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.
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:
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).
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
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.
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 :)
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:
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):
which seems like an increment operator, but 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!
There is no need for such ambiguity. It makes parsing harder. It makes it hard to recognize that it's actually an element with some semantics attached and not just a weird decoration.
Also, a lot of capitalization.
TLA+ programs, from typographic perspective, look really, really awful.
There are languages which just look bad due to weird typographical choices of their authors. Usually because they use symbols in the context the font author never expected them to be used. For example, any language that uses camel-case or pascal-case is an affront to typography because font authors don't anticipate capital letters in the middle of the word surrounded by minuscule letters. Similarly, nobody expects sequences of "=" signs or ":" written adjacent to the following word rather than previous one etc.
Some look really awful due to extreme abuse of punctuation (C++ would be a good example with all the &&::<<<*_>>,<**>> stuff), others look very repetitive to the point that they make you lose focus (eg. Pascal-style language which have "if-then-else-end if" going on where sometimes for many lines you just keep reading the "cargo train" of "end, end, end, end if, end". Lisps are also in this category because they usually look too uniform.
TLA+ looks like a Fortran program from the 60's formatted on a physical typewriter with all sorts of weird uses of the small number of available glyphs to substitute for the actual typographical thing that wasn't available to the author.
https://github.com/Viasat/salt
Successor: https://github.com/Viasat/halite
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.