TLA⁺ is more than a DSL for breadth-first search
1–3 of 3 posts
Re: TLA⁺ is more than a DSL for breadth-first search
#2Quint [1] is a specification language heavily based on TLA+ but without the mathy syntax people have issues with, and without inheriting the tool problems of a language that was never designed to be "code" (i.e. Quint has types and good IDE support).
Quint also has the concept of a run, where users can guide the "searcher" to a specific set of executions, so it works really well as a BF/DF* searcher, which is it's focus (it doesn't support refinement or proofs, at least for now).
So yeah, if you are curious for a language that supersedes TLA+, you should definitely give Quint a try :)
* BF through model checking, DF through bounded random simulation
Re: TLA⁺ is more than a DSL for breadth-first search
#3Quint [1] is a specification language heavily based on TLA+ but without the mathy syntax people have issues with, and without inheriting the tool problems of a language that was never designed to be "code" (i.e. Quint has types and good IDE support). Quint also has the concept of a run, where users can guide the "searcher" to a specific set of executions, so it works really well as a BF/DF* searcher, which is it's fo…
Quint looks like _exactly_ what I’ve been looking for. It’s all the good parts of TLA+, but with sensible types, and a focus on executability.
I understand that executability makes the language much less _powerful_ in a mathematical sense. But it’s such a benefit in all other ways that I think we should focus on the specification that we can write that are also executable.