Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in op

Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in optimization and code generation: http://compcert.inria.fr/doc/html/Compiler.html http://compcert.inria.fr/doc/html/Compiler.html As one particular example, register allocation is performed by an untrusted oracle that may not even terminate, and then verified a posteriori: http://compcert.inria.fr/doc/html/Allocation.html http://compcert.inria.fr/doc/html/Allocation.html They proved a traditional register allocator correct in a paper (https://www.cs.princeton.edu/~appel/papers/regalloc.pdf https://www.cs.princeton.edu/~appel/papers/regalloc.pdf), but I guess there are practical reasons why they are not using it in CompCert by default.