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/

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.