Goodbye ProofGeneral, again

A couple of weeks ago Holger Gast announced the first release of the new interactive interface for Isabelle theorem prover. I was planning to write its review, but I decided not to as Jesus Aransay’s wrote a post on the Isabelle mailing list that  pretty much summarizes what would be in that review.

For me the lack of proper display of mathematical symbols and subscripts is a show stopper. You can’t write mathematics without that. I hope that will be resolved soon and I3P will be an excellent replacement for ProofGeneral.

Goodbye ProofGeneral

Some recent messages on the Isabelle mailing list bring the information that the Isabelle team is working on a new interface for Isabelle and possibly other provers that will replace Emacs based ProofGeneral. The new interface will be written in Scala. Scala is an multiparadigm language (OO and functional) that runs on JVM. This is an interesting choice of technology that suggests something about the design goals (I am speculating again). Applications writen in Scala can run on any platform that has JVM. In particular, one can write applets in Scala that can be run in a browser. Scala is a general purpose language, but seems to be particularly good for web programming. There are a couple of web programming frameworks written in Scala, Lift being the most popular, competing with Rails. So the new interface will be multiplatform and easy to integrate with web applications (wiki?). Hopefully this will make Isabelle proving environment closer to being network transparent – a user interface, possibly running in a browser and sending formalized text for verification to an Isabelle server located (possibly) on a different host with dependencies scattered all over the internet.