[bugarela]

It is in deed tricky, but we tried. We fully kept the semantics of TLA+, so the same mental model people still need to learn (at least a little), but a syntax that is much more familiar to engineers/programmers.

This is Quint [1], a different syntax for TLA+ with some extra tooling (type checker, CLI, evaluator, REPL, VSCode extension, testing framework, etc) which can be transpiled to TLA+ (which is a very direct translation, as the semantics is the same [2]) and therefore make use of the TLA+ tools as well (mainly the model checkers).

I think this is far from the same level of "unreadableness" than TLA+, and it makes formal methods much more approachable. It would be great if you could take a look and tell me whether you agree.

[1]: https://quint-lang.org/ [2]: https://quint-lang.org/docs/lang

[bvrmn]

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.

[bugarela]

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

[lucyjojo]

wow this is great!

do you cover all of that TLA can do??

TLA syntax is simply a pain to type on my keyboard and it has been a hurdle for the longest time...