Comment by riku_iki

I would argue is that some portion of ecosystem should be readable by humans.

In programming engineering we already have this: there is human readable high-level code, and there is assembler and lots of auto-generated code.

In proof system we could have the same: key concepts/theorems should be encoded in human readable form, but no need for human to read through millions of generated lines.