I have been thinking about writing a small "book" (html w/.jpg diagrams) titled something like, "Metamath For Programmers", which with yellow and black on the cover would be similar in both intent and implementation to "Metamath For Dummies".
One reason this is a good idea is that I cannot yet begin writing mmj3 because I don't know enough about what are the interesting things that it should do.
Another reason is that the scholarly papers such as "AN AUTOMATIC THEOREM PROVER FOR SUBSTITUTION AND DETACHMENT SYSTEMS" by Jeremy George Peterson and Norm's "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" are almost unapproachable and inscrutable without extensive background preparation (e.g. "An inference rule related to Rule D is the resolution principle of J. A. Robinson [16], commonly used in automated theorem proving. A deductive system of logic whose inference rules are resolution together with the related rules of factoring and paramodulation can be considered finitely axiomatized in our sense and can produce clauses (theorems) that correspond to Skolemizations of theorems of predicate calculus with equality. But such a system is not “deduction complete” so that, for example, G¨odel’s completeness theorem fails to hold [21].")
Furthermore, I believe that (geometric) tree-based algorithms, if described using diagrams and words, are easier to understand -- are more scrutable – than the "loop and GOTO" algorithms such as Robinson's unification algorithm. And the tree algorithms are not just more scrutable they are more general, being so to speak, "language agnostic" (this builds upon the Metamath system which has only these built-in inference rules: typed valid simultaneous substitution and hypothesis reiteration (as in "dummylink").) Now that I have done the work to make mmj2 I can almost appreciate Condensed Detachement and Rule D, but there is no reason for others to have to suffer through all that. It should be possible to begin with Metamath and let interested students delve into its archeological history if they so desire.
Another example: I have just arrived at the conclusion that mmj2's StepUnifier?.java algorithm produces the Most General Unification if the input proof step contains only Work Variables. Therefore, I can now describe a method of unification based on recursive unification of parse sub-trees and variable renaming. This approach is based on performing sub-unifications until an inconsistency is found or there are no more subtrees: if unification of the set of formulas "A" with the set of formulas "B" produces no inconsistencies, then the resulting set of simultaneous substitutions from A into B are "consistent". Type checking of substitutions is required for the "validity" portion of the description, as is $d checking which is outside the scope of the StepUnifier?'s mandate (it might be possible to integrate $d checking – that is a subject worthy of more research.)
(((I am also interested because Peterson's paper goes in exactly the same direction I went with my idea about generating all possible theorems and then writing them out in the most compact form possible as a list of numbers. His "theorem prover" is in actuality a theorem generator, and note that his primary "heuristic" was limiting the length of stored formulas during the generation process.)))
I can also equate the Metamath Proof Verification Algorithm directly to the other tree-based unification algorithm which does not use Work Variables (in ProofUnifier?.java). They are the same thing except that the former uses RPN lists and the latter uses trees. And, as with unification, the fact that the Metamath algorithm may be more efficient is less relevant in this era of fast, cheap computers if the tree methods are easier to understand (anyway, once the tree method is explained and accepted, it is easy to demonstrate that a valid tree can be converted to an RPN list, and vice-versa.)
I think that the beauty and elegance of Metamath is offset – for programmers – by the unnecessarily difficult background material which can be explained in a more modern style. Then with the subjects mentioned above as a foundation, along with other topics such as building a grammar from a .mm file and parsing, the way will be clear for others to perform much additional work! For example:
I believe that once the mysterious and inscrutable parts of Metamath are better explained it is likely that many more programmers will begin work to advance the state of the art (and America can defeat the armies of EU-funded programmers working on Omega :-)
FYI, I started diagramming the MObj class hierarchy, with small, possible forward-looking "enhancements", and it took quite a lot of work. That hierarchy isn't even 1/3 of the mmj2 classes either. The amount of work involved in just re-documenting mmj2, to say nothing of designing an mmj3, or writing a book is mind-boggling. It makes my ass hurt just thinking about how long I sat at this desk writing the mmj2 code. I have to say, I am pretty happy that we have mmj2 now considering how much work went into it and the fact that it actually works pretty well.
That said, the project of analyzing Metamath in view of everything we have discovered (i.e. figured out what Norm already knew) is definitely worthwhile. There are still many discoveries to be made!
BTW, Dia version 0.96.1 has some bugs. Lots of shapes, especially grievously, the UML shapes, are not resizeable. The little black squares should be green, but instead are just static and useless. I ended up doing my diagrams using the basic drawing elements and the UML arrows. Sigh. (Better than paper and pencil, but worse than Visio (which I paid for once, but which was rendered unusable in WinXP?, for some reason.))