[johncolanduoni]

I'm referring to the operational semantics[1]. This doesn't require any tacit knowledge to fix the language past what the horizontal line and definitional equality symbols mean (it's entirely in the form of purely syntactic "given this, you can write this"), but it won't be remotely helpful to teach you what the syntax reductions mean or how to use them. If you're never heard of lambdas, you could technically still "use" them in the sense a computer can, but good luck figuring out that they represent functions. It wouldn't fit any sensible definition of "understanding".

My point isn't that these things are easy to learn because their presentations are so brief; personally, dependent typing took me a long time for me to wrap my head around. What I think the briefness of the operational semantics in combination with the examples of things people have built within them suggest is that they're very versatile. Even if only people working on language level features bother to learn them, the utility of their creations (all without needing to move to another language or introduce possibly incompatible extensions) is a huge asset.

[1]: https://en.wikipedia.org/wiki/Operational_semantics