Comment by bvrmn
2 months ago
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.
Thanks for the feedback! We actually improved the documentation a lot in the last year, and we host it in a website now: [1]
Most of the documentation doesn't mention TLA+ anymore, as it is focused on new programmers coming to formal methods with no prior experience with it. I agree it was very confusing before!
Other than that, if I can argue against some of your points: 1. Quint brings more than just type checking (better IDE diagnostics, better REPL, better CLI, and runs that work like tests) [2] 2. The translation rules between Quint and TLA+ are actually very straightfoward [3], specially if we stay in the common idiom of TLA+. 3. This is more subjective, but a few people using Quint have reported to really like isolating the state machine into the "action" mode and then defining the protocol in "pure def"s. I understand what you mean by "leaky" and a part of me agrees with that, but, in practice, we are seeing real benefits on this side.
Again, thank you for your points - there's some stuff in your feedback I haven't heard before, and it's great to have a new perspective.
[1]: https://quint-lang.org/docs/language-basics
[2]: https://quint-lang.org/docs/faq#how-does-quint-compare-to-tl...
[3]: https://quint-lang.org/docs/lang