bugarela

7 ms·

1.
Our formal methods tool can be a company – because of AI(quint.sh)
8 points by bugarela 5mo ago|0 comments
2.
by bugarela 5mo 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
3.
by bugarela 6mo 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
4.
by bugarela 6mo 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/informalsyst
5.
Towards a Solution for Cognitive Debt(quint-lang.org)
2 points by bugarela 6mo ago|0 comments
6.
Quint LLM Kit for writing and using formal specifications(github.com)
11 points by bugarela 7mo ago|0 comments
7.
by bugarela 9mo 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 m
8.
Choreo: Choreograph Distributed Protocols on Quint(quint-lang.org)
3 points by bugarela 1y ago|1 comments
9.
by bugarela 1y 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 starte
10.
by bugarela 1y 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 m
11.
by bugarela 1y ago
You can also use Model-Based Testing (MBT) and produce (arbitrarily many) tests for your production code from your (model-checked) model.
12.
by bugarela 1y 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 di
13.
by bugarela 2y ago
Super cool! You might also like Quint if you give it a try: https://quint-lang.org/ 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 exa
14.
by bugarela 2y ago
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 an
15.
by bugarela 2y ago
Two main things: alternative syntax and tooling 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 w
16.
by bugarela 2y ago
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
17.
by bugarela 2y ago
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) techni
18.
by bugarela 3y ago
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! [1]: https://
19.
Holiday protocols: secret santa with Quint(github.com)
8 points by bugarela 3y ago|1 comments
20.
by bugarela 3y ago
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 i
21.
by 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&#x
22.
by bugarela 3y ago
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.
23.
by bugarela 3y ago
I didn't take a very deep look yet, but this might be similar to https://github.com/pfeodrippe/recife
24.
by 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