Comment by logicchains

Have you heard of https://cakeml.org/? It's a self-hosting formally verified compiler.