Metamath responds

Norm Megill, the man behind Metamath, responded to my recent post about Metamath and hygienic macros:

You are correct that substitution in Metamath is the simple replacement of a variable with a (well-formed) expression and thus isn't hygienic, in Scheme's terminology. In logic, the term used for “hygienic substitution” is “proper substitution,” which Metamath does not implement directly.

Instead, Metamath natively implements a simpler concept of “disjoint variables” as an optional proviso on an axiom (and inherited by theorems), that will forbid certain substitutions. In more standard terminology, this means, for example, that (if the axiom says so) a certain bound variable may not occur in a wff. In this case, the wff may have to be transformed, in the proof, to an equivalent wff with the bound variable renamed before we are allowed to substitute it for the wff variable of the axiom. In effect, the work of renaming bound variables, in order to make a sound (hygienic) substitution, is done by the proof itself rather than by the proof verifier. This simplifies the underlying primitive concepts needed by the Metamath language itself, with a consequence that the proof verifier can be very simple.

How simple is Metamath's verifier? About 300 lines of Python does the trick.

Simplicity is not the motivation in Lisp; in fact Lisp is generally more complicated than Scheme. Rather, Lisp programs actually take advantage of symbols getting crossed. (If you know Lisp macros, you know what I mean, and if you don't, I can't easily explain it.) I know Metamath does something similar in at least one place: its definition of proper substitution.

([y / x]φ ↔ ((x = y → φ) ∧ ∃x(x = y ∧ φ)))

I wonder if similar tricks are used elsewhere.