Quint(quint-lang.org)

115 pointsby todsacerdotivor 2 Jahren26 comments

https://quint-lang.org/

26 comments

chriscbrvor 2 Jahren

Going off of the example on the home page, the language reminds me a lot of Alloy, a model checking language. Alloy lets you describe facts about some discrete system and check for the existence (or nonexistence) of properties within those systems. If you expect some property to hold and it doesn't, Alloy will automatically produce a counter-example for you. Here's an example of a program modeling a file system:

  sig FSObject { parent: lone Dir }
  sig Dir extends FSObject { contents: set FSObject }
  sig File extends FSObject { }

  // A directory is the parent of its contents
  fact { all d: Dir, o: d.contents | o.parent = d }

  // All file system objects are either files or directories
  fact { File + Dir = FSObject }

  // There exists a root
  one sig Root extends Dir { } { no parent }

  // File system is connected
  fact { FSObject in Root.*contents }

  // Every fs object is in at most one directory
  assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }

I initially thought these model checking languages were purely academic in nature. But then a curious problem came up when I was working at AWS where folks were complaining that IAM policies generated by our library were sometimes growing to be too large in size (usually the limit was a few KB) - often due to redundant statements.

To solve this, a coworker implemented some code for merging IAM policies -- though the merging processe wasn't trivial because IAM policies can have both "Resources" and "NotResources", "Actions" and "NotActions", "Principals" and "NotPrincipals" etc. So to prove the algorithm was correct, he wrote up a short Alloy specification[1] (roughly mapping to the library code) that proved if two policy statements were merged, it wouldn't change the security posture. As a new engineer to the team, I'll just say that it blew my mind that this was possible -- actually using proofs to achieve goals in industry.

Needless to say, I'm curious to dive into Quint's differences and what kinds of models/specifications it excels with.

[1] https://github.com/aws/aws-cdk/blob/main/packages/aws-cdk-li...

cl3mischvor 2 Jahren

> describe facts about some discrete system and check for the existence (or nonexistence) of properties

To me this sounds like Logic Programming and I immediately think of Prolog. Is it fair to compare them?

sirwhinesalotvor 2 Jahren

Yes, but the implementation is very different. These model checkers aren't turing complete, and because of that they can give some strong guarantees about what they can and cannot do. Prolog? Shift some things around and watch your program suddenly run forever or so slowly as to be useless.

If you want to mess around with something very prolog like but using similar kinds of underlying tech to these model checkers, try playing around with ASP solvers like Clingo/Clasp or DLV

hwaynevor 2 Jahren

Protip: instead of writing

    (a.resource in b.resource and a.action in b.action and a.principal in b.principal) or

You can write

    {
     a.resource in b.resource
     a.action in b.action
     a.principle in b.principle
    } or // ...

(Also instead of `(some principal) iff not (some notPrincipal)` you can write `some principle <=> no notPrinciple`. Alloy has a lot of cool syntactic sugar!)

CGamesPlayvor 2 Jahren

So, with projects like this, once you've got the specification verified, how do you then make sure your implementation fits the specification?

skybrianvor 2 Jahren

I'm guessing it's the same way you ensure that your code implements a specification written in English.

But at least you know the specification is consistent.

sriram_malharvor 2 Jahren

Some projects make it possible for you to generate verified code from the specification.

There is usefulness to these tools even if the implementation is a separate beast. At a minimum, they allow you to test drive your ideas in particularly thorny areas such as concurrency and security. Forcing you to think hard about a secure kernel or a library of data structures is a good thing in and of itself. You only have to give such core libraries this kind of anal attention, not to the layers built atop.

sirwhinesalotvor 2 Jahren

Some model checkers like CBMC annotate C code directly. Others can generate piles of tests. But usually just knowing your requirements are consistent and exactly how the algorithm has to behave to work as intended goes a long way!

bugarelavor 2 Jahren

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.

There is one example for this as a Rust test: https://github.com/informalsystems/quint-sandbox/blob/main/S...

hwaynevor 2 Jahren

In addition to what everybody else is saying about the value of having a spec at all, there's a lot of exciting developments now in using a spec to generate a test suite, which is way simpler than using a spec to generate production code. Example: https://arxiv.org/abs/2006.00915

ChrisArchitectvor 2 Jahren

More discussion on a submission from one of the devs:

https://news.ycombinator.com/item?id=38694278

lordofgibbonsvor 2 Jahren

I guess I'll go first and ask: when and where should I use this?

chipxsdvor 2 Jahren

Looks like there's more information in their readme: https://github.com/informalsystems/quint

> Quint is a modern specification language that is a particularly good fit for distributed systems, such as blockchain protocols, distributed databases, and p2p protocols. Quint combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art type checking and development tooling.

steegovor 2 Jahren

From what I’m reading, it’s a specification language that’s an alternative to TLA+ with a more familiar syntax.

Here’s an overview presentation by the creator:

https://youtu.be/OZIX8rs-kOA?si=b2U_fNB0U2wDoR-F

bugarelavor 2 Jahren

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].

[1]: https://protocols-made-fun.com/consensus/matterlabs/quint/sp... [2]: https://informal.systems/blog/interchain-meet-starknet [3]: https://lamport.azurewebsites.net/tla/formal-methods-amazon....

sriram_malharvor 2 Jahren

I'm unable to see the difference between this and TLA. Is it "merely" (*) an alternate syntax?

What is the value-add to TLA or PlusCal? For example, fizzbee (https://fizzbee.io) offers python syntax and data structures, which makes it very intuitive.

(*) No snark intended; a good syntax can give you joy.

bugarelavor 2 Jahren

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

sriram_malharvor 2 Jahren

Thank you for your explanation.

lou1306vor 2 Jahren

Indeed it seems that the verification relies on Apalache, which is an alternate (symbolic) model checker for TLA.

TLA (well, TLA+) gives access to a richer specification language, as it allows e.g., to express liveness properties (informally defined as "something good happens at some point") as opposed to just safety ("nothing bad ever happens"). But the model checker does not use symbolic techniques so it may suffer on larger systems.

Personally I also find Quint to be way more readable/intuitive but your mileage may vary.

sriram_malharvor 2 Jahren

Thanks. More readable/intuitive is always welcome. I'll give it a try.

jayaprabhakarvor 2 Jahren

https://FizzBee.io is not just a syntax transpiler, but a complete implementation. It uses starlark language (a Python variant) for specification. In addition to behavioral modeling like TLA+, Quint etc, it supports probabilistic and performance modeling. Generates state and sequence diagrams automatically.

kreyenborgivor 2 Jahren

https://wikidiff.com/quint/quaint just to clear that up

ultra_nickvor 2 Jahren

With LLMs getting smarter every day, the next generation might be writing specs like this instead of actual code.

pasquinellivor 2 Jahren

as a total aside, that informal systems logo could use some tightening up. that f in particular looks floppy.

9991vor 2 Jahren

Bike shedding of the highest order.

nineteen999vor 2 Jahren

We're gonna need a bigger bike.