Bram pointed me to this thesis on implementing real numbers within HOL. I heartily recommend this thesis to people following this thread (if any). It's very interesting to compare to Metamath's construction of the reals. Unfortunately, these constructions are not compatible. One significant difference is that Metamath seems to support partial functions, so 1/0 is not in the range of the divide function, while HOL wants to have total functions within the type, so 1/0 must have some value (Harrison chooses 0 to simpify the details). As such, proofs from one probably can't be easily ported to the other without serious handwork.
I feel I understand Metamath reasonably well now. It has some issues, but it's overwhelming strength is that it's simple. For example, I believe that a fully function proof verifier could be done in about 300 lines of Python. I wonder how many lines of Python a corresponding verifier for HOL would be; I'd guess around an order of magnitude larger. That kind of difference has profound implications. Norm Megill is certainly to be commended for the "simplicity engineering" he's put into Metamath.
For the purpose of putting doing Web-distributed proofs, Metamath has a few shortcomings. I think they can be fixed, especially given the underlying simplicity. I'll talk about these problems and possible fixes over the next few days.
Definitions in Metamath have two closely related problems. Definitions are introduced exactly the same way as axioms. As such, it's far from obvious when a definition is "safe". For example, you could add definitions for the untyped lambda calculus, which would introduce the Russell set paradox. The second problem is that there is a single namespace for newly defined constants. You wouldn't be able to combine proofs from two different sources if they defined the same constant two different ways.
Here's my proposal to fix these problems. Choose a highly restricted subclass of definitions that is clearly safe. For example, you could say that any definition of the form "newconst x y z = A" or "newconst x y z <-> phi", with newconst not appearing in A or phi, is acceptable. I propose to introduce new syntax that clearly identifies such definitions. You could use existing syntax, so that such definitions become axioms, but can be checked easily, or you could have other syntax that sets the new constant apart from its "macro expansion". That's a style preference.
Now let's talk about namespaces. I have a strong preference for using hashes as global names, because (assuming the hash function is strong), you don't get collisions. As such, it should be possible to mix together arbitrary proofs without danger. Here's an outline proposal.
Take the definition axiom, and replace the newly defined constant with some token, say $_. Hash the result. That is the "global name". When you're developing proofs, you'll probably want a (more or less) human-readable "pet name", but this is actually irrelevant for verification. Here's an example in Metamath notation.
Here's Metamath's definition of the empty set
$( Declare the symbol for the empty or null set. $)
$c (/) $. $( null set $)
$( Extend class notation to include the empty set. $)
c0 $a class (/) $.
$( Designate x as a set variable for use within the null set definition. $)
$v x $.
$f set x $.
$( Define the empty set. $)
dfnul2 $a |- (/) = { x | -. x = x } $.
So here's what gets hashed:
$a class $_ $. $f set x $. $a |- $_ = { x | -. x = x } $.
Take the SHA-1 hash of this string. Then I propose that #274b1294a7d734a6e3badbf094190f46166159e4 can be used (as both a label and a constant, as these namespaces are independent) whenever the empty set is needed. A proof file would of course bind this string to a shorter name, such as (/). When importing a proof file from another, the binding would be local to the file. (Currently, Metamath has only a file include facility similar to C's preprocessor #include, but an import facility with better namespace management would be quite a straightforward addition, especially considering that Metamath already has ${ $} scoping syntax).
Obviously, there are some details to be worked out, particularly nailing down exactly what gets hashed, but I think the idea is sound.
Schooling
Alan's Mindstorms arrived a couple of days ago. These promise to be quite fun (and of course educational :). So far, he's settling into first grade very easily. We begin the half-homeschooling starting on Monday.
Even so, I get the sense that Max is going to be the one most into computers. He's learning the OS X interface impressively well. Last time we resumed the computer, a folder was highlighted, and he said, "it's clicked." Then, when I ran Stuffit to unpack a game demo, he noted the icon and said, "it's squishing it." He's also the one that said, "I love Alan's 'puter".