I did an eval of Quint about year ago and did not find it compelling. It constantly refers to TLA+ and doesn't bring much benefits except typing. Syntax tries to cover underlying fact that state machine is expressed in terms of logic and math using "understandable" for programmers concept but it's very leaky in the end. IMHO "assign" is quite hard to grok without TLA experience. Documentation is scarce.
The most frustrating part it's hard to use with TLA+ background. I know how to do something in TLA but have no clue with Quint because translation rules aren't direct and obvious.
On the other hand it's a way better than PlusCal!
But I'm heavily biased. Please take this "critique" as a mumble from TLA+ initiated duckling.
The most frustrating part it's hard to use with TLA+ background. I know how to do something in TLA but have no clue with Quint because translation rules aren't direct and obvious.
On the other hand it's a way better than PlusCal!
But I'm heavily biased. Please take this "critique" as a mumble from TLA+ initiated duckling.