Re:CompCert – A formally verified C compiler
by snazz on Tuesday January 22, 2019 @09:48AM
(#18968575)
The 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.
[ Parent
| on HN ]
Re:CompCert – A formally verified C compiler
by kiriakasis on Tuesday January 22, 2019 @01:53PM
(#18971115)
In 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...