3 ms·
Not completely: > about 90% of the compiler’s algorithms (including all optimizations and all code generation algorithms) are proved correct in Coq, but the re
by sobriquet9 5y ago
Not completely:
> about 90% of the compiler’s algorithms (including all optimizations and all code generation algorithms) are proved correct in Coq, but the remaining 10% (including elaboration, presimplifications, assembling and linking) are not verified