As Aaron Swartz suggests, I downloaded Red Hat 8.0 using BitTorrent. From casper, the performance was amazingly good: around 800-1000 kB/s. I've long felt that free software ISO's were a killer app for this code. Unfortunately, it seems not to be in anybody's business interest to push this angle, because the relative convenience factor of getting a boxed CD is pretty much gone if you can get full-bandwidth downloads.
Incidentally, the GUI version crashed randomly on me, but the command line version behaved fine.
Red Hat 8.0
I like it. I like it a lot.
I installed it on a spare partition on spectre, just to give it a whirl. This time, I kept a log of usability issues and bugs. I ran into quite a few, but I think overall the system hangs togther pretty well. Obviously, people put a lot of work into making the desktop a good experience as a whole. This is rare and highly welcome in the oft-fragmented world of free software.
I was pleased that it detected (almost) all my hardware correctly, including the Audigy soundcard and the dual CPU's. I'll have to add the (serial) Wacom pad by hand, but that's not bad at all.
There's a good chance I'll put this on my laptop too.
GnomeMeeting
One of the perks of RH 8.0 is that installing GnomeMeeting 0.93.1 was near-trivial. As I understand, this is pretty difficult software to get running from scratch. I wasn't looking forward to herding a Gnome 2 development environment onto my machine. To have it Just Work is a nice treat.
I'm not sure the rest of our team will be able to use GnomeMeeting effectively just yet. Among other things, the H.323 nonsense prevents it from working behind a vanilla firewall. That's a problem TeamSpeak seems to have solved by using a nonstandard protocol.
I went to #gnomemeeting on irc.gnome.org and got personal help from Damian Sandras, principal author of the program. He was very nice, and of course this level of community involvement is exactly the reason why free software is so good. I want GnomeMeeting (or at least some free VoIP solution) to win.
ZFC vs HOL
I got a very nice email from Robert Solovay in response to my last entry. He patiently explained to me that you can prove the consistency of HOL using ZFC theory, which means that ZFC is strictly more powerful. Gödel's second completeness theorem means that no system can prove its own consistency. Thanks.
A lot of this stuff still seems fairly murky to me, but I feel the waters clearing. I had some minor epiphanies over the past few days. For one, I now see a clean separation between two parts of making a Web-friendly mathematical system. One part is the translation between various proof systems, so as not to limit people too much. The other part is to arrange the inputs, outputs, and immediate files to make it maximally easy to share over the Web. These are quite separate: it's not hard to imagine proof format translators still stuck in the teletype interaction mode characteristic to HOL, or a Web-friendly system based on any one of the major logical systems. The latter seems easier to me, actually. I'm still a novice at the heavy mathematics behind logic and proofs, but I feel I know a lot about the Web and about how people can collaborate over the Internet.
The other insight has to do with the issue of making "conservative" proofs designed for portability. I think I can now answer the question: what are the natural numbers?
Well, what are the natural numbers?
This may be a bit sketchy, because the ideas still feel a bit raw.
At heart, the natural numbers are the Peano axioms. But just stating the axioms isn't quite enough to make them useful in a proof system. Among other things, it's dangerous to just add axioms lest they introduce inconsistency.
So, you build a construction of the naturals using native primitives of your proof system. For each axiom, you prove a theorem. In the Metamath approach, you then do everything in terms of this construction.
But what HOL does for type definitions is better. Essentially, by making a construction, you're proving that the axioms are consistent with the primitive logic. It doesn't really matter which construction you use, as long as you end up with the same axioms.
In fact, what I just said is a key meta-result. The usual interpretation of proofs in these formal systems is that they prove a single statement. But here, an abstract proof using only the Peano axioms can easily be transformed into a concrete proof, just by substituting in the actual construction.
Meta-logic in general makes me uncomfortable, but in this case I think it's what's needed to address deep problems of portability. In particular, I think it solves the problem of multiple different axiomatizations of the same basic concept. Your "construction" can go between two equivalent axiom sets just as easily as to a construction in your primitives. You keep your proofs abstract, but at the end you check them in some specific formal framework: ZFC if all you care about is the truth of the proposition, and "smaller" systems such as HOL if you want to check portability.
I don't think I've communicated the idea well. It's also a bit half-baked. I've only talked about naturals, but there are other things, especially functions, that are harder to treat this way. But I do think I'm on to something here.