(no title)
bugarela | 1 year ago
Some things that a programmer would take for granted are not available in TLA+ tooling, but are for Quint. The biggest examples: syntax and type checking in the IDE as you type, standard CLI with standard error reporting, LSP (Language Server Protocol) support (so you can use "Go To Definition" in your IDE).
In addition to that, Quint has a way to define tests (runs) and it makes it so it's easy to execute a specification, which is not normally possible in a natural way.
TLA+ has more advanced mathematical expressions that are not supported in Quint. This is on purpose. There are many things you can write in TLA+ but not in Quint, but those are the things that most people would only write by accident and be extremely confused by the results. The people who would write those knowing what they mean will probably like the Mathy syntax of TLA+ much better than Quint, so they should just use TLA+.
sriram_malhar|1 year ago