Comment by nickpsecurity

There's a new extractor that can output C from Coq. There's also multiple compilers for each language you can extract to. My solution was to do diverse compilation where multiple compilers, OS's, and ISA's compiled the compiler. Then you just run it through itself on each one. Use end result that most agree on.