Just after writing my last post, a trip to Japan suddenly materialized, to pitch Ghostscript to printer companies. Between dealing with moving stuff, preparing for the trip, actually going, and then going to Quaker Yearly Meeting, I haven't had much time left over for, say, blogging.
My crazy schedule doesn't wind down for another six weeks or so (I've got trips to Chicago for Print 05, and to Holland to visit Oce, lined up), but at least I've got a little break now. Well, after Linux World, anyway! I'll be at the linuxprinting.org booth on Tuesday and Thursday. If you're in the area, it'll be a good time to touch base, see my printing work, and maybe even sneak a peek at my PhD thesis work on curves.
I've been continuing to work slowly but steadily on Ghilbert. This last week, I completed the proof of findes in my portable axiomatization (the axioms used in this proof are pure predicate calculus with equality plus the Peano axioms; no sets needed as in the Metamath version).
I'm finding formal logic to be deeply satisfying, but so far am happy working on it as a personal, private project. I don't find it easy to explain to people exactly why I think Ghilbert is the right approach, but it feels more and more right the more I play with it.
The web presence is very sparse now, but as the project progresses it will become primarily Web-based, with the ability to browse and post bits of proof online. Ultimately, I think Ghilbert's potential for collaboration will be its greatest strength. An ironic goal, isn't it, for a project with such a lame web page.