Highlight actions

We could usesemantic highlighting to have different fontfaces for actions by consulting the effects. I'm not sure how to make that not look completely messy, we should be careful, but I thin that might be very useful if we get it right.

Tasks

It is possible to read arbitrary files and detect tasks, and these tasks can be run from the VSCode command pallete. Imagine we have some mdx-like (or some other configuration format like .toml files as atomkraft is using), detect tasks from that and have commands likeCheck liveness property,Simulate malicious example, etc. Those can be completely spec-specific since they are defined by a configuration file, as the example is specific to Quint typescript project.

Notebooks

For protocol specification, we can have a markdown renderer that parses and processes Quint code blocks. The original.md file should be readable by itself so people don't depend on the plugin to read the file.

Code completion

Using type information + dot call format, we can offercode completion like any OOP language. That is, given a setS, typingS. shows operators that take sets as their first argument.

Example from vscode docs:

Type hints

After opening parenthesis, we can show an operator's type (and maybe effect?) signature to help users remember which arguments are needed. PS: Currently, our built-in operators don't have names for their arguments, but it's much helpful to show signatures with named arguments (index: int as opposed to onlyint)

Image fromvscode docs

Type annotation inference

We can infer types for the operators, but as in many programming languages, it's nice if the user explicitly annotates top-level operators so they can be sure their intentions are met. We can automate that task by providing a button for annotating an operator with it's inferred type, so the user only has to check for it's correction and then benefit from a established type contract.

PS: idk why my gif recorder is so dark, sorry

Code Navigation

Easily find where a symbol is defined or all references to a symbol.

Example fromvscode docs:

Maybe we can render diagrams for individual actions, similar to what the ANTLR extension does

Under the heading of support for literate programming.

@konnov noted that there are some standard practices spec authors (in particular
protocol designers) can adopt that would improve the quality usefulness of
specs. E.g.,

• Examples (usingrun, so these also amount to tests of the spec)
• Invariants
• Formalization in quint (as opposed to only describing something in a paragraph)

Support for literate formal specs could include templates and linting to
automate encouragement of enforcement of these practices.