I stumbled on MLcompcert which connects miniml with compcert. Sort of like cakeml, but for Coq. I'm surprised I didn't hear about this before.
Does anyone know more about the project?
I remember looking at documentation/papers, but I don't think the "pure" source was ever released
Last updated: Aug 19 2022 at 19:03 UTC