I have not been following closely this area for many years, but I know
systems have existed for a very long time to capture semantics or help
translation. The first system for creating interpreters based on
denotational semantics was SIS created by Peter Mosses around
1980. Around the same time, programmable structured editors and some multilanguage programming environments started being
used for program transformation and even program translation between
high-level languages, based on abstract syntax manipulation, since the mid-late seventies. Centaur
(Kahn et alii) was such a system circa 1990. However, though some such systems did use formal semantics for various purposes, the translations I
know of were programmed more or less by hand. There have been
compilers based on formal semantics, but I think it is already pretty
hard just to prove them correct. Coq has been used for that and it is still on-going work.
Even if you manage to capture the semantics of both your languages,
trying to infer from that a translator from one to the other is likely
to be beyond current technology. For one thing, programming languages
do not use exactly the same high level concepts, and that is what
makes translation very difficult. Compiling, which is a form of translation to a target language produces code in a very low level language, not very readable, as the structure of the program is no longer explicited.
It is true that some systems based on Curry-Howard isomorphism and type theory, such as Coq, can assist the production of programs by extracting them from a proof of their specification. But these are carefully tailored systems, with an adequate specification formalism. I doubt that a program written in another programming language could serve as such a specification within the current state of the art.
I fear that the best you can hope for is the equivalent of a compiler to machine code: the
source language will be translated in some kind of machine code
expressed with an elementary and naive use of the target language. I doubt this is what you have in