3 ms·
Verifiable compiler means given a C source code their compiler-generated assembly code or IL code is verifiable that it functions the same as the source code.
by amir734jj 8y ago
Verifiable compiler means given a C source code their compiler-generated assembly code or IL code is verifiable that it functions the same as the source code.
- snazz 8y agoThe GP was asking how the compiler deals with the fact that it itself must be bootstrapped with another, unverified compiler before it can compile its own code.
- kiriakasis 8y agoIn this case the bootstrapping problem is slightly different. What you are bootstrapping is not the compiler but the verification, in coq this would be trusting that the ocaml extracted code is correct by the coq proofs. But I might be wrong, there are a lot of nuances and I do not know them all...