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
=. 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.)