Invisible functions are everywhere in mathematics -- we talk about things being equal in such a cavalier way. This doesn't matter much when doing mathematics, but it matters a little in computer science. I wrote a blog post trying to explain:
Conversation
This is incidental to the main point, but it's maybe worth pointing out that, unlike the assembly language metaphor, the lower level language of set theory doesn't necessarily give us "faster/more efficient code" for mathematical formalizations.
1
2
I think it might just make for a larger de Bruijn factor!
1
On the other hand, I think the metamath library compiles in about ten seconds flat, whereas Lean's maths library takes about half an hour! Not that we ever compile it nowadays, we just download compiled mathlib binaries :D
1
I wonder how a similar logic to Lean's implemented in Metamath would compare speed-wise. It might be interesting to see if some foundations are inherently "faster" than others..
1
Might the type system need to be encoded as an intermediate layer, slightly slowing compilation? I don't know enough to say.
1
It's on the reading list! It's not exactly what I had in mind, IIUC one would still need to specify an actual DTT logic in it to make comparisons with say set.mm(0). Still it's really impressive, and its speed is astounding!