2 ms·
The language specification and the compiler would have to be proven correct first. Which is increasingly difficult with higher level languages and with optimiz
by billswift 17y ago
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.
- gdp 17y agoFor this project, that's assumed. Provided you have some kind of formal semantics, you can define translations. And in fact, Adam Chlipala's work on certified compilers show that it's not impossible. http://adam.chlipala.net/papers/CtpcPLDI07/ http://adam.chlipala.net/papers/CtpcPLDI07/ (there are subsequent papers too, but that's probably a good place to start).