Viewing profile — bugarela

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 …

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 lea…

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 tha…

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 …

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 …

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,…

You can also use Model-Based Testing (MBT) and produce (arbitrarily many) tests for your production code from your (model-checked) model.

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 fam…

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…

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 ne…

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: syn…

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 o…

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, bu…

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 f…

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 lan…

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.d…

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.

I didn't take a very deep look yet, but this might be similar to https://github.com/pfeodrippe/recife

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+…