What are the pros and cons of continuous checking over keychord-triggered checking?

Question

As far as I know, the default configuration for the Lean VSCode plugin checks the code continuously, and so even when the user is in the middle of typing an expression, Lean will immediately report a syntax error. In contrast, proof assistants like Agda defaults to checking the code only when the user presses a key combination.

I understand that this can be changed through configuration, and you can temporarily "freeze" the proof state. But what is the design consideration behind this choice? In what ways do users have better / worse experience using continuous checking?

Answer 1

In 2017 and 2018 I learned three languages, Rust, Scala, and Lean. All three are similar in that they enforce strong typing constraints in order to guarantee the correctness of code which can be checked at compile time instead of run time. They also use advanced features such as type classes and macros to make the language more flexible, but at the same time “safe”. All this makes compiling take longer, but if it does compile (or type check) then you know it has a better chance of working as desired.

When I first tried Rust, I just used a basic editor with syntax highlighting, and the command line to compile and run my code. It was incredibly frustrating. The compiler complained about one thing and I had to go back and fix it. I often had to resorting to tricks to learn what the type of a variable was.

When I learned Scala for work, it was strongly recommended I use the IntelliJ IDE which has an amazing Scala interface. Unlike my Rust experience, the IDE made it so much easier to learn Scala and progress. Most importantly the turn around time was much faster. Instead of waiting for a whole file to compile, I could just see instantly when I had a compile error. It is basically the same as modern continuous spell checkers. The error is unobtrusive—to me at least—and I can address it then if I know the problem (for example I made a typo) or later if I don’t.

It feels collaborative. At every point the IDE is helping me with all the little things. What is the type of this variable? Click and see? What is the order I need to put in arguments to this function? Click and see? Did I misspell something or use the wrong function? It will let me know. Is my code going to compile? I already know. If it has no red squiggles then yes.

A coworker of mine once confessed that she used to think “IDEs are for chumps”, but after her experience with Scala and IntelliJ she feels very different now.

After that Scala experience I can’t imagine not using these features when programming. I now use IDEs with language server features even for Python programming. It makes me much faster. The editors catch common typos of mine like swapping == and =. It also makes it easy to change a variable name, or refactor a piece of code without fear that I’m going to make a ton of painful little errors. It gives me a lot more power. When I returned to Rust, I looked into the Rust language server (which plugs into IDEs like VS Code). This made a night and day difference. I now am able to see not only my errors, but also get a better feel for how Rust works and what things are ok and not okay to do. There is almost zero delay between typing and feedback.

I’ve been focusing on non-theorem provers in my answer since I don’t want to make this a Lean verse “the others” post. Lean happens to have continuous checking, but so do many of the new proof assistants like Arend and Metamath Zero. It, in many ways, just seems like an obvious choice, at least for proof assistant designers who can afford to put in the time to make it work, and users who generally like interactivity. (Of course, users like Dima Pasechnik who prefer the command line would understandably hate being forced to use an IDE. While users, like myself, now get annoyed when I have to push a key command to check another step of code in an older theorem prover.)

Also, Andrej Bauer makes a good point that the current systems which don’t have continuous checking are perfectly usable. This one feature is likely not a reason to switch tools. Nonetheless, I think all heavily used computer languages will have this feature in the next 10 years (including Agda and Coq). There are just a large number of users who like it, and it seems for them (at least for me for sure) to increase productivity and mastery of the language.

Now, why don't other theorem provers like Agda and Coq have this asynchronous continuous checking? I can only speculate, but as Andrej’s answer suggests, they likely were created before continuous checking was feasible and common. Also, it is likely not the easiest thing to implement and likely harder to add on after the fact. (Creating continuous checking language servers for Python for example is a big business, including PyCharm (the sister to IntelliJ) as well as VS Code’s proprietary Pylance plugin. This suggests that a lot of work must go into making these quality tools.). Nonetheless, it does look like both Agda and Coq are adding support for the language server protocol (and maybe with that continuous checking). See here for Agda. See here for Coq.

Also, it isn’t enough to have continuous checking. It has to be performant. Even Lean’s checking can sometimes stall. This is especially common if one is looking at a file deep inside mathlib. (One consideration with continuous checking is what to do if a file is being edited and not saved yet. VS code doesn’t save edits automatically but IntelliJ does. I wonder if this impacts how the continuous checking works in each IDE.) In Lean, if a file is open and being edited, then any dependencies on that file need to be rechecked if they are used in another open file. Sometimes Lean will even recheck the open file when it is not being edited which is annoying. This can cause massive performance issues in Lean that require a restart. I’m sure it can be fixed (edit: and Sebastian Ullrich informed me that it is fixed in Lean 4), but it does show the downsides of continuous checking in that it is hard to get right. In general, no continuous checking is better than bad continuous checking.

I’ll just end with another comment about IDEs. I think IDEs (especially "native" apps like VS Code and IntelliJ, but also Emacs and Vim) have come a long way in the past 5 to 10 years. For example, it used to be that the only way to do remote development (i.e. you can work with a theorem prover or programming language on another server) was to use the text-only versions of Emacs or Vim from the command line. But now seamless remote development in a GUI environment is also available in VS Code (for free) and IntelliJ (for a price). Further, VS Code, IntelliJ, Emacs (and I assume Vim) also have good git integration and a built-in terminal for whenever you need the command line.

Similarly, the language server protocol has also made it a lot easier to integrate continuous checking tools with all IDEs. For example, any editor which supports LSP can use Rust’s language server. There is no need for a separate Rust plugin or Rust editor. This can move the development of these tools back to the language designers and make them integrate tighter with the compiler. (Edit: Sebastian Ullrich pointed out that to take full advantage of the Rust analyzer, which goes beyond LSP, one still needs a separate plugin, and the same is true for Lean and other ITPs.)

Answer 2

I can report on my personal user experiences with Coq, Agda and Lean:

1. Coq checks an initial segment of the file (and it does not matter what garbage fills the rest of the file). The Emacs mode can be set up so that Coq automatically checks the next input as soon as the user types in the period . (which indicates the end of the command). I don't like that, it feels like the machine is rushing me. I much prefer the mode in which I tell Coq what precisely to check.

2. Agda checks the entire file. The user may request re-checking of the file, or they may just submit the solution to one of the goals (in which case, I think, it only checks the submitted fragment, but I am not sure). In practice, checking the whole file is not a problem. If there is garbage at the bottom of the file, it has to be commented out, and Agda mode has shortcuts for doing so.

3. Lean is designed to work more like the programming language IDEs that can check fragments of code, rather than whole files. By default it proactively checks the user input, which works well in most situations. The user may also choose a more passive strategy.

One should understand that Coq is much older than Agda, which is much older than Lean. They were designed in different times when people did not have computers with $2^n$ cores and $2^{2^m}$ kilobytes of memory. It is fair to say that Lean's interface is natural evolution of the older interfaces.

I can tell you from experience that telling the machine "please check this here" is no big deal. It feels completely natural to tell Coq up to what point it should check the file. Telling Agda when to check things gives me the feeling of being in the driver's seat. Lean's eager checking gives a different feel, it is more like having someone looking at what you are doing and giving you instant feedback. I am pretty sure beginners would in general prefer Lean's mode, as they do not have to learn when to tell the proof assistant to look at their work (but they learn quickly, at least my students do).

There have been occasions when I had to turn off Lean interactive mode because it went off and started compiling huge amounts of stuff, and eventually hogged available memory. But this was a rather specific situation when I was experimenting with processing a very large number of small files (thousands). It would be nice if there were a way of telling Lean "never ever check anything in this folder unless I tell you to" (for all I know it can do that).

In conclusion, I would say that the precise details of the interactive mode are not very important, but I cannot imagine working non-interactively.

Answer 3

The following is more of a response to Kevin's answer than the answer to the question.

---

Lean's VSCode IDE-like interface aggressively over-instruments the interaction with the user - this is and always will be a subjective view.

All these auto-completions, popups, quick changes in syntax highlighting might be extremely distractive for some users. E.g. I find I can only work with VSCode - even if I use its TeX plugin writing a paper - in "zen mode" - where most of menus and tabs are hidden, and it still is often too much interaction.

It is naive to think that as much interaction as possible is the best for everyone.

Answer 4

I do not really understand this question. The only advantage which "check up until this point and then stop" has over continuous checking is that you get to freeze the state and examine it whilst writing your next line of code. However if this ability is incorporated into your continuous checking system then you have a system which has all the benefits of "check up until this point and then stop" whilst retaining the many benefits of continuous checking (i.e. making it much easier to write code).

Lean with VS Code offers this functionality. You can "pin" states if you want, i.e. keep the state you want to see (e.g. because you want to refer to it whilst thinking about what you want to write next) whilst also simultaneously enjoying the benefits of continuous checking (i.e. you can see two goal states at once when a state is pinned; your current continuously-checked goal and the pinned static one). Pin a state by hitting the pin icon above it.

Lean with VS Code also offers the ability to pause the output of continuous checking and to turn it off completely, however these are options which I use far less often.