Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit

Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. Makarius Wenzel, UITP 2010.

After several decades, most proof assistants are still centered around TTY-based interaction in a tight read-eval-print loop. Even well-known Emacs modes for such provers follow this synchronous model based on single commands with immediate response, meaning that the editor waits for the prover after each command. There have been some attempts to re-implement prover interfaces in big IDE frameworks, while keeping the old interaction model. Can we do better than that?

Ten years ago, the Isabelle/Isar proof language already emphasized the idea of proof document (structured text) instead of proof script (sequence of commands), although the implementation was still emulating TTY interaction in order to be able to work with the then emerging Proof General interface. After some recent reworking of Isabelle internals, to support parallel processing of theories and proofs, the original idea of structured document processing has surfaced again.

Isabelle versions from 2009 or later already provide some support for interactive proof documents with asynchronous checking, which awaits to be connected to a suitable editor framework or full-scale IDE. The remaining problem is how to do that systematically, without having to specify and implement complex protocols for prover interaction.

This is the point where we introduce the new Isabelle/Scala layer, which is meant to expose certain aspects of Isabelle/ML to the outside world. The Scala language (by Martin Odersky) is sufficiently close to ML in order to model well-known prover concepts conveniently, but Scala also runs on the JVM and can access existing Java libraries directly. By building more and more external system wrapping for Isabelle in Scala, we eventually reach the point where we can integrate the prover seamlessly into existing IDEs (say Netbeans).

To avoid getting side-tracked by IDE platform complexity, our current experiments are focused on jEdit, which is a powerful editor framework written in Java that can be easily extended by plugin modules. Our plugins are written again in Scala for our convenience, and to leverage the Scala actor library for parallel and interactive programming. Thanks to the Isabelle/Scala layer, the Isabelle/jEdit implementation is very small and simple.

I thought this was a nice paper on the pragmatics of incremental, interactive proof editing. I've suspected for a while that as programming languages and IDEs grow more sophisticated and do more computationally-intensive checks at compile time (including but not limited to theorem proving), it will become similarly important to design our languages to support modular and incremental analysis.

However, IDE designs also need more experimentation, and unfortunately the choice of IDEs to extend seem to be limited to archaic systems like Emacs or industrial behemoths like Eclipse or Visual Studio, both of which constrain the scope for new design -- Emacs is too limited, and the API surface of Eclipse/VS is just too big and irregular. (Agda-mode for Emacs is a heroic but somewhat terrifying piece of elisp.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Clojure seen from ML

It is a very minor point indeed, but I smiled at their quick description of Clojure.

Apart from various scripting languages such as Groovy, Jython, JRuby, two functional languages have gained attention in the mainstream world: Clojure (roughly an untyped version of Haskell using LISP notation), and Scala with its sophisticated integration of higher-order functional object-oriented programming and direct access to existing Java class libraries.

Agda-mode not so bad

I'm surprised about your comment "Agda-mode for Emacs is a heroic but somewhat terrifying piece of elisp.". In fact, Agda-mode's elisp part is about 3k LOC, and basically delegates as much as possible to the Haskell layer it communicates with. Under the hood, it runs Agda in a GHCi session where it can issue Haskell commands to interact with it. As much as possible of the work is done in Haskell code, reusing many parts of Agda in the process.

Anyway, I'm not saying Emacs offers the ideal plugin developers' API, and I'm not a fan of elisp myself, but trust me, as far as elisp goes, Agda-mode is very okay.

First, I want to make clear

First, I want to make clear that I'm pointing to Agda-mode as noteworthy for the excellence of its IDE interface. It's a vastly better interface than many other programming languages offer, and deserves accolades for that.

However, I think your comment makes my point for me, as to the complexity of the implementation. It's not just that 3 different languages are involved, but that ghci is, too!


Finally had a chance to read this and look at the author's previous work.

Anyone who wants to read the code can get Isabelle2011.