I got a nice email from Michael Norrish, suggesting that maybe HOL is not as difficult as I suspected. The core of HOL Light is only about 1000 lines of ML. That's an appealing level of simplicity. Of course, ML is particularly well suited for doing HOL-style logic, but that hardly counts as a strike against it!
Without meaning any disrespect for other projects such as Mizar, QED, Mathweb, NuPrl, etc., for the stuff I'm interested in, HOL and Metamath are definitely the two systems of interest. They're both simple, they're both founded on mature work in mathematical logic, and there's enough mathematics done in both to make comparisons useful.
Unfortunately, the two systems are different enough to pose major compatibility problems. At heart, functions are different beasts. In ZF(C) set theory, they're essentially untyped, and allowed to be partial. They can be hugely infinite, but can't take themselves as arguments. Thus, even such a simple and familiar expression such as lambda x.x can't be directly expressed as a ZF set.
HOL functions, on the other hand, are typed, but total within that type. Thus, the function lambda x. 1/x is problematic. Harrison's construction of the reals in HOL arbitrarily takes 1/0 = 0. The trick of polymorphic types lets you apply a function to itself, with just enough limitations to avoid the paradoxes. So lambda x.x is back in the club.
I get the feeling that there's been work on connecting the two flavors of formal system, but it seems technical and difficult to me. This is disappointing.
In any case, I feel this interest in logic burning itself out for now. I'm sure I'll come back to it later; it's been an interest of mine for a long time. I still feel that a Web-centered distributed proof repository could be a very interesting thing, and that the tools I'm comfortable with could be applied well. But what I do not need right now is another big project.
The big DeviceN merge happened, and it's not too bad. There are still some regressions, but they're settling down. A big chunk of my recent work has been putting together a framework to test whether 6-color DeviceN rendering is consistent with plain CMYK. I'm becoming an even firmer believer in testing, and I think that graphics rendering systems are particularly suitable for automated testing.
I'm craving a chunk of time to sit down and write Fitz design ideas, but with the Ghostscript 8.0 release process taking all my time, it's not been easy. Even so, some aspects of the design seem to be coming into relatively clear focus, even as details on things like font and text rendering seem elusive. I'm particularly excited about the design of the runtime discipline. In particular, it should be a lot easier to understand and integrate with other systems than the current Ghostscript runtime discipline. I don't see a lot of work on conscious design for runtimes; more commonly, designs inherit runtimes from somewhere else (language, library, predecessor). As such, I'm hoping that the runtime document will make interesting reading even for people not in the market for a graphics rendering library.