Start with "What and why"

[gisborne]

I followed a link to Quint from a community of interest (Future of Coding Slack).

The link didn't discuss what Quint is, and I'm sad to see that the documentation for Quint doesn't appear to, either. Which seems odd.

This might be something I'm interested in, but after a few minutes poking around, I still have no idea what problems this solves, or in what way it's different, or really much of anything.

[bugarela]

Regarding the what: it says pretty much everywhere that it is an executable specification language, which is what it is. Perhaps it would be useful to add pointers to what a specification language is (like this one from Wikipedia).

The why is a bigger story, which I tried making as concise as possible through an example. The website also has a big "find bug" button that is supposed to help getting this motivation out. But we do have larger pieces of content about the why spread all across the documentation, so it might be useful to group them better and link them for people who are just arriving.

Thanks for your feedback! I'm realizing that there are many different needs from people looking at our landing page and readme. It's hard to satisfy all of it, but we should at least have pointers to different pieces of information so people can find what they are looking for in this sense.

[gisborne]

The link I followed was to this page: https://quint-lang.org/docs/lang

That didn’t tell me anything about what this was, but I clicked “Introduction”. Some introduction. That was when I created this bug report.

Now that I know a little more, I want to know:

• is this Turing Complete?
• is this a general-purpose language (ML was developed for writing compilers, but is also a terrific general-purpose language; this might be like that?)

I still don’t know.

[bugarela]

I see. I don't think we specifically talk about this things anywhere.

As a language, it is Turing complete. However, keep in mind that both the simulator and the model checker will only consider executions of up to --max-steps and there is no recursion, so in practice it is impossible to have infinite loops.

It is a general-purpose specification language. It is not a programming language, so you can't use it for things you'd use a programming languages for. For example, there is no IO.

[konnov]

Hi @gisborne! I am not developing Quint atm. Just curious, whether you could point the developers to a good example of a website that does a better job at presenting a programming language than Quint?

[gisborne]

https://ziglang.org/