[bugarela]

I mostly agree with this, with one caveat: There is a group of people that want to specify executable things, mainly for the sake of specifying it. They might use a programming language for that, but doing so with a specification language instead can bring some benefits, including model checking in the case of Quint and TLA+.

I don't think Quint users are only focused on model checker, as you imply. It is very useful to specify things. However, in the world of software, turns out that people want to specify things that actually execute, and won't need a way to express things that don't.

[pron]

> but doing so with a specification language instead can bring some benefits, including model checking in the case of Quint and TLA+.

I was referring to benefits that only a rich specification language like TLA+ (or Coq or Isabelle) could bring, although TLA+ is more naturally expressive than the others. Model checking is nice and very useful, but just the rich formal specification is at least as useful in itself. Like most people, I was drawn to TLA+ for the model checking, but after spending a lot of time with it, I realised that model checking was its least interesting benefit even though it's its best marketing. It's really cute and useful that there are model checkers for TLA+, but I'd used SPIN and Pathfinder before, and they were cool, too. What set TLA+ apart for me was the way it let me specify and improve my designs, not the fact that it happened to have a model checker (although without the model checker I probably would have never given it a chance).

> turns out that people want to specify things that actually execute, and won't need a way to express things that don't.

Absolutely. And others want to specify things that cannot possibly execute, because if they could they would make for a lousy specification from a very practical perspective (it's of the utmost practical importance to be able to say: this distributed protocol requires O(lg n) messages, and yet it's not something you can easily model-check), and you can't have both. A model-checked specification is often not a good enough specification, and a good specification is not something you can model-check.

So in the practical world of software it turns out there are people who want to model check, and there are people who want to write good specifications, both groups are positively tiny but the former is larger. Neither is fully served by something made for the other. Something that's great at being fully model-checkable cannot be really good for specification and vice versa. I'm all for more languages that are more fully more checkable, but it's important to acknowledge that such languages are less practical for rich specification. Both specification and model-checking are practical concerns, but there's always a tradeoff.