> you will have to prove the compiler Strictly speaking you don't - that's one of two approaches. Fortunately, the CompCert compiler already exists if you want

> you will have to prove the compiler Strictly speaking you don't - that's one of two approaches. Fortunately, the CompCert compiler already exists if you want to go the route you describe. The alternative to use a non-verified compiler, but verify that the generated code corresponds to the model. This is the route the seL4 project took. They used GCC, but verified the correctness of the code it generated.