I am on the dev team for this project and would be happy to answer any questions and/or take note of any critical feedback :)<p>Here's a bit more detail:<p>Quint is a modern, executable 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 static analysis and development tooling.
> We have covered all the aspects of our "Hello, world!" example. Actually, we could have written a much shorter example, but it would not demonstrate the distinctive features of Quint.<p>Ouch! When I am trying to wrap my head around a new tool, I want a series of examples starting with <i>the absolute simplest possible example</i>.<p>If I can see only one new concept demonstrated at a time, each in the simplest context possible, I can quickly develop a clear understanding. By quickly, I mean a solid understanding in minutes.<p>Anything else just generates questions (and am I even thinking the right questions?) at a faster rate than lightbulbs.
I'm trying to understand what is the difference between this and using TLA.<p>For example, what is the difference between "robust theoretical basis of the Temporal Logic of Actions (TLA)" and "state-of-the-art static analysis"?<p>Sorry, I'm not an expert in TLA, but I thought that static analysis was basically what it was used for.
One thing that was a demotivating factor (for me) about TLA+ is the syntax (I later realized that there's a more high-level language that looks more like a programming language and less like markup: PlusCal, but it was too late :). This looks a lot nicer.
This is something I really wanted to build when I learned about TLA+ over a year ago. Taking the core idea into a modern language and toolings. Congratulations that you actually did it!
Recommended introduction talk for context:<p><a href="https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=GatewaytoCosmos" rel="nofollow noreferrer">https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=Gatew...</a><p>TLDR: compileable modeling language to model the high-level protocol of your blockchain (or any distributed system). It's a "digitalization" step of plain written English protocol specifications to code.