I have not been following this area for a very long time, 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, interactive environments started being used for program transformation and even program translation between high-level languages, based on abstract syntax manipulation. Centaur (Kahn et alii) was such a system circa 1990. However the translations I know of were programmed more or less by hand. There have been compilers based on formal semantics, but I think it was already pretty hard just to prove them correct (Coq has been used for that)

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. The best you may get is that the source language will be translated in some kind of machine code expressed in the second language. I doubt this is what you have in mind.

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 mind.