Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.

How would you improve it? (Also note that this is not the language mathematicians will actually work with - that's more like https://www.youtube.com/watch?v=b-RfoUuQpAQ)

Similarly, for Metamath Zero, MM1 compiles down to the MM0 base language: https://www.youtube.com/watch?v=A7WfrW7-ifw

I think it's just a neat example that helps one understand how the verifier itself works at the most fundamental level.