The language specification and the compiler would have to be proven correct first. Which is increasingly difficult with higher level languages and with optimizing compilers. The critical aspect is that the MACHINE CODE has to be correct. That is one of the reasons the problem is so hard.