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.
Yeah, I understand it's hard to find the balance here. I'd imagine you feel the need to ship at the same time as writing about it. For me, the post you shared in your reply as well as in the OP have been expanded to be about 3-4x as long as they need to be, and I'm going to assume you're using AI to generate them due to the writing style. My feedback is to consider writing shorter posts, but doing it by hand -- your prose style here is friendly, engaging and direct. I wish that your articles were the same.
TL;DR: I feel like my time is being wasted when I read AI-written articles, so I stop reading. Do with my anecdote what you will!
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.
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.
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.
I did an eval of Quint about year ago and did not find it compelling. It constantly refers to TLA+ and doesn't bring much benefits except typing. Syntax tries to cover underlying fact that state machine is expressed in terms of logic and math using "understandable" for programmers concept but it's very leaky in the end. IMHO "assign" is quite hard to grok without TLA experience. Documentation is scarce.
The most frustrating part it's hard to use with TLA+ background. I know how to do something in TLA but have no clue with Quint because translation rules aren't direct and obvious.
On the other hand it's a way better than PlusCal!
But I'm heavily biased. Please take this "critique" as a mumble from TLA+ initiated duckling.
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.
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
Quint looks like _exactly_ what I’ve been looking for. It’s all the good parts of TLA+, but with sensible types, and a focus on executability.
I understand that executability makes the language much less _powerful_ in a mathematical sense. But it’s such a benefit in all other ways that I think we should focus on the specification that we can write that are also executable.
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.
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.
reply