Reading `hol.mm` made me grateful for Lean 4's general purpose programming.
I get the string substitution focus, and respect what metamath has achieved, but the bridge Lean 4 makes wrt systems programming has left quite an impression.
I wonder how many people mostly see mathlib4 & think that's the one prescribed route (ala Rust) when one of Lean 4's under-documented super powers is the ease with which you can roll your own light-weight low to zero overhead domain-specialized constructs that are also trivial to prove because of the dependent type system.
(Perhaps more for verified functional systems than deep math.)
I get the string substitution focus, and respect what metamath has achieved, but the bridge Lean 4 makes wrt systems programming has left quite an impression.
I wonder how many people mostly see mathlib4 & think that's the one prescribed route (ala Rust) when one of Lean 4's under-documented super powers is the ease with which you can roll your own light-weight low to zero overhead domain-specialized constructs that are also trivial to prove because of the dependent type system.
(Perhaps more for verified functional systems than deep math.)