Isabelle team has released Isabelle 2011. The upgrade was not as smooth for me as the previous one. The new ProofGeneral didn’t work with Xemacs shipped with Ubuntu 9.10, giving a “file mode specification error”. I tried then the new jEdit interface that found that ZF logic is missing. Indeed, the Linux bundle does not contain precompiled ZF logic. It was not a big problem, I built it with “build ZF”.
The jEdit interface (see the screenshot) represents a new approach based on “continuous proving” concept. While I think it is very interesting technologically, it turned out extremely slow on my Athlon 64 1.8GHz with ony 512MB of RAM. Apparently all this proving in the background with keeping multiple versions of the document was just too much. It would be usable if it was possible to temporarily disable the continuous proving feature, but unfortunately this is not supported yet.
Then I turned to the latest I3P version 1.0.10 that supports Isabelle2011. This seems to be the best choice for me. The previous problems with Isabelle symbols display have been fixed. The interface is somewhat similar to ProofGeneral which makes it easier to get used to. The subscripts (Isabelle’s \<^isub> markup) are still not displayed, but this is also the case for the jEdit interface.
On a an unrelated topic, Mark Adams gave a good answer to the question “Why is is so difficult to write complete (computer verifiable) proofs?” posted on MathOverflow.The answer is an accurate description of the process of writing a formal proof. The only thing I disagree with is his opinion that “there are very few people in the world capable of doing this stage effectively for large proofs (perhaps just John Harrison, Tom Hales and Georges Gonthier)”, the stage being creating coherent formalisable versions of standard proofs as found in math publications. It is indeed rather rare skill, but still there are hundreds of people who are able to effectively create large formal proofs, for any sensible definition of “effectively” and “large”. Those are people who contribute to Mizar, publish in the Archive of Formal Proofs or write extensive libraries for proof checkers that they created, like Norman Megill of Metamath or Rob Arthan of ProofPower.
In other news, Jeremy Bem is writing a “lightweight proof assistant based on standard set theory and Hindley-Milner type theory”. Layering type theory on top of untyped set theory seems to be popular these days – Sebastian Reichelt’s HLM is another very interesting example. HLM deserves a separate blog post which I hope to write soon.