1. Rewriting systems are very useful tools. One of the things I learned from this post was about the existence of FullEquationalProof [1], which I think is pretty darn neat and super useful.
2. This post is imbued with a latent metaphysics that is somewhat common in formal mathematics and will invariably come out at relevant meetings/conferences after a few glasses of wine. Not this instantiation in particular, but a generally similar sort of metaphysics. I've always gotten church vibes from that sort of thing. (I never "got" church.)
I never got the "emergent properties have special aesthetic and nearly spiritual significance" or "everything is just an <insert structure here>" cognitive confusion that so many mathematicians (especially formalists) seem to have.
But the way that it happens does make sense. Intellectual curiosity is a valid work selection strategy and sometimes invention/discovery requires a leap of faith. Developing a predisposition to spiritual thought patterns while doing work that requires a leap of faith makes sense, I guess, but it's something I warn young mathematicians to guard against.
But then, I'm also not allergic to fava beans. Maybe math-as-spirituality and believing beans are evil are also just useful tools.
[1] https://reference.wolfram.com/language/ref/FindEquationalPro...