I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place: https://pit-cla

I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place: https://pit-claudel.fr/clement/ https://pit-claudel.fr/clement/ As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.