Re:Quint
by lordofgibbons on Tuesday July 30, 2024 @11:58PM
(#41116313)
I guess I'll go first and ask: when and where should I use this?
[ Parent
| on HN ]
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.
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:
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....