Hey, if you were write a high-level spec for a programming language, I'm guessing you'd choose to use a logical framework for the core? Like this, for instance: arxiv.org/abs/2106.01484? How would you describe elaboration from the surface lang to the core language?
Conversation
I'm using ‘specification’ more in the sense of ‘documenting how to implement the programming language’, as opposed to a formal or mechanised specification specification with proofs, etc. Something like the WASM spec, for example: webassembly.github.io/spec/core/