This is so cool, I'll definitely be playing with in over the weekend. I meant to put Quint and D&D together in some similar ideas before but never found the time, so I love to see this coming alive from someone else <3
Interesting, thank you! I feel the same about avoiding reading AI stuff, that's my worry here. In OP, I had way too much content and had AI help me reduce the size of if. But I learned a lot since then and some parts of the post bother me a bit now.
For the second post, it was a wall of prose that my colleague, Josef, wrote (I'm pretty sure without AI). I added the more concrete example sections and then asked AI to suggest some heading names to break down the prose, and I'm assuming this was my mistake as the headings are the first thing people read and AI loves headings. I always broke down text in headings before AI, this suck haha.
Anyway, I'll definitely increase my neurotic levels about this. It's not worth at all to rush things if it will make the post more empty to read in any way.
Hey! We were not really sure how to pass on the information back when I wrote this in November, but since then we've packaged an opensourced all agents and AI stuff involved in that post: https://github.com/informalsystems/quint-llm-kit
It's true what they say that it is easy to make a demo in AI, but super hard to turn demo into some product or thing other people can use. We are trying :) but also, most posts I read on this topic are just philosophical and give absolutely nothing you can learn and use. We are trying to provide concrete ideas on the things we are exploring, like in our newest post: https://quint-lang.org/posts/cognitive_debt
I'm also a bit happy you see some sales drive in that post since I'm 100% technical and trying to be more sales-inclined. I'm learning to find the balance. If it helps, it's more like I'm so extremely hyped about this and want to convince people to use it. And everything we built so far is open source, so it's really about selling the cool idea of formal methods at this point.
Me and my team have recently done an experiment [1] that is pretty aligned with this idea. We took a complex change our colleagues wanted to make to a consensus engine and tried a workflow where Quint formal specifications would be in the middle of prompts and code, and it worked out much better than we imagined. I'm personally very excited about the opportunities for formal methods in this new era.
The Quint (specification language based on TLA+) team just launched Choreo: a framework to get started writing specs for distributed systems, leveraging some known techniques such as the message soup. This should help more people get started with formal specifications without having to study so much about non-determinism and state space optimization.
Thanks for the feedback! We actually improved the documentation a lot in the last year, and we host it in a website now: [1]
Most of the documentation doesn't mention TLA+ anymore, as it is focused on new programmers coming to formal methods with no prior experience with it. I agree it was very confusing before!
Other than that, if I can argue against some of your points:
1. Quint brings more than just type checking (better IDE diagnostics, better REPL, better CLI, and runs that work like tests) [2]
2. The translation rules between Quint and TLA+ are actually very straightfoward [3], specially if we stay in the common idiom of TLA+.
3. This is more subjective, but a few people using Quint have reported to really like isolating the state machine into the "action" mode and then defining the protocol in "pure def"s. I understand what you mean by "leaky" and a part of me agrees with that, but, in practice, we are seeing real benefits on this side.
Again, thank you for your points - there's some stuff in your feedback I haven't heard before, and it's great to have a new perspective.
It is in deed tricky, but we tried. We fully kept the semantics of TLA+, so the same mental model people still need to learn (at least a little), but a syntax that is much more familiar to engineers/programmers.
This is Quint [1], a different syntax for TLA+ with some extra tooling (type checker, CLI, evaluator, REPL, VSCode extension, testing framework, etc) which can be transpiled to TLA+ (which is a very direct translation, as the semantics is the same [2]) and therefore make use of the TLA+ tools as well (mainly the model checkers).
I think this is far from the same level of "unreadableness" than TLA+, and it makes formal methods much more approachable. It would be great if you could take a look and tell me whether you agree.
This looks like a great example, I'll try to find some time to write a version of it in Quint. I have mentioned DB migration as an example of two phase commit usage before, but never as a standalone spec like this. It's definitely the kind of problem that made me anxious in the past, which means it's a good fit for formal verification :)
Quint [1] is a specification language heavily based on TLA+ but without the mathy syntax people have issues with, and without inheriting the tool problems of a language that was never designed to be "code" (i.e. Quint has types and good IDE support).
Quint also has the concept of a run, where users can guide the "searcher" to a specific set of executions, so it works really well as a BF/DF* searcher, which is it's focus (it doesn't support refinement or proofs, at least for now).
So yeah, if you are curious for a language that supersedes TLA+, you should definitely give Quint a try :)
* BF through model checking, DF through bounded random simulation
Some things that a programmer would take for granted are not available in TLA+ tooling, but are for Quint. The biggest examples: syntax and type checking in the IDE as you type, standard CLI with standard error reporting, LSP (Language Server Protocol) support (so you can use "Go To Definition" in your IDE).
In addition to that, Quint has a way to define tests (runs) and it makes it so it's easy to execute a specification, which is not normally possible in a natural way.
TLA+ has more advanced mathematical expressions that are not supported in Quint. This is on purpose. There are many things you can write in TLA+ but not in Quint, but those are the things that most people would only write by accident and be extremely confused by the results. The people who would write those knowing what they mean will probably like the Mathy syntax of TLA+ much better than Quint, so they should just use TLA+.
It really shines in protocol design, see [1] and [2] (both very recent posts). But you can use it for anything you are not confident enough about being correct. This happens very often when working with distributed systems, where there are way too many factors to consider.
More generally, TLA+ (the base language for Quint - Quint can transpile to TLA+) was used at AWS to find bugs and make aggressive optimizations in several services [3].
If you have a specification that resembles your implementation well enough (which is not naturally the case, as keeping specifications on a higher level is almost always better, but can be done), you can use Model-Based Testing (MBT) techniques to increase confidence that your implementation matches the specification.
For example, you can ask Quint to generate a bunch of traces (executions) for you in JSON and then parse those to run tests in the implementation. If your trace is [{action: deposit(10), result: ok}, {action: withdraw(20), result: Error}], you can have an sort of integration test for your implementation that asserts that calling deposit(10) should result in ok and then calling withdraw(20) subsequently should result in an error.
Hi! I wrote a blogpost exploring a formal specification in Quint [1] for the secret santa game, and verifying some of its properties with Apalache [2].
Hope you enjoy it, and any feedback is welcome. Happy holidays!
I mostly agree with this, with one caveat: There is a group of people that want to specify executable things, mainly for the sake of specifying it. They might use a programming language for that, but doing so with a specification language instead can bring some benefits, including model checking in the case of Quint and TLA+.
I don't think Quint users are only focused on model checker, as you imply. It is very useful to specify things. However, in the world of software, turns out that people want to specify things that actually execute, and won't need a way to express things that don't.
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+.
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.
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.