4 ms·

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

• chipxsd 2y ago
  Looks like there's more information in their readme: https://github.com/informalsystems/quint 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.
• steego 2y ago
  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 https://youtu.be/OZIX8rs-kOA?si=b2U_fNB0U2wDoR-F
• 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 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/specification/modelchecking/2024/07/29/chonkybft.html https://protocols-made-fun.com/consensus/matterlabs/quint/sp... [2]: https://informal.systems/blog/interchain-meet-starknet https://informal.systems/blog/interchain-meet-starknet [3]: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....