Comment by 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