For 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

For 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).