I'm trying to understand what is the difference between this and using TLA.
For example, what is the difference between "robust theoretical basis of the Temporal Logic of Actions (TLA)" and "state-of-the-art static analysis"?
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!
This looks really nice. It's the first thing I have seen that appears to be approachable from a developer's perspective.
How do you compare this with Alloy?
Recommended introduction talk for context:
https://www.youtube.com/watch?v=OZIX8rs-kOA&ab_channel=Gatew...
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.
this sounds like something you'd plug into an LLM asA AGI
Interesting
> 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.
Ouch! When I am trying to wrap my head around a new tool, I want a series of examples starting with the absolute simplest possible example.
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.
Anything else just generates questions (and am I even thinking the right questions?) at a faster rate than lightbulbs.