bugarela
Joined 2 years ago
Karma
31
Submissions
27
Member since
Dec 8
Lead developer of Quint https://quint-lang.org/
View on Hacker NewsRecent submissions
Comment · 6 months ago
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
Comment · 7 months ago
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.
Comment · 7 months ago
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.
Comment · 10 months ago
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.
Comment · 1 year ago
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.
Comment · 1 year ago
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.
[1]: https://quint-lang.org/docs/language-basics
[2]: https://quint-lang.org/docs/faq#how-does-quint-compare-to-tl...
Comment · 1 year ago
You can also use Model-Based Testing (MBT) and produce (arbitrarily many) tests for your production code from your (model-checked) model.
Comment · 1 year ago
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.
[1]: https://quint-lang.org/ [2]: https://quint-lang.org/docs/lang