VSCode extension ideas

[bugarela]

I'm creating this discussion to keep track of all our ideas for the VSCode extension. Let's try to keep one idea per top-level comment to keep things organized.

[bugarela]

Highlight actions

We could use semantic 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.

[bugarela]

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 like Check 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.

[bugarela]

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.

[konnov]

How about the opposite: The users could write markdown in Quint comments. We could also render that in nice HTML. This would look like literate programming.

[bugarela]

Code completion

Using type information + dot call format, we can offer code completion like any OOP language. That is, given a set S, typing S. shows operators that take sets as their first argument.

Example from vscode docs:

[bugarela]

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 only int)

Image from vscode docs

[bugarela]

Instead of showing effects on hover, we can actually show the mode, as typescript shows const before the name in this example:

Actions can show the variables they update with the action<...> syntax

[bugarela]

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

[konnov]

This would be a really cool feature!

[bugarela]

Code Navigation

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

Example from vscode docs:

[bugarela]

Done in #546

[bugarela]

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

[konnov]

This should be relatively easy to implement now, since we have the call graph. Though it may be that people would find "Find all references" more useful than the graph (they are hard to render and hard to navigate).

[bugarela]

I was not thinking about this in terms of the call graph, but in terms of state machine transitions. I'm not sure if it is feasible, just raising the idea. For the call graph, I agree that "Go to References" is more useful.

[shonfeder]

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 (using run, 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.