2
$\begingroup$

I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there exists more general workbenches for this.

E.g. one can formally specify programming language, that is clear. But are there any tools that can be used for capturing the formal semantics for formally specified language. It is obvious that the operational semantics is the most suitable for industrial programming languages. And - if semantics is specified then the translation from one programming language into other can be done at the meta-level. I guess, that this maybe too hard for C-to-Java translation, but it should work for more modest, recent languages that are created by academia.

I have heard about Maude, but I guess that there can be something more. My experience is that Google can not replace bibliographies or suggestions from community. Thanks.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

We have been working on one for the last few years: Lem, a higher-order, typed language with backends for OCaml, Coq, Isabelle/HOL, HOL4, LaTeX and HTML. Lem has been used internally in the group to formalise various machine models (PowerPC, ARM, and so on), memory models (the C memory model, etc.), programming language semantics (OCaml Light), and so on.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Have you attempted the kind of translation from one language to another envisioned by the OP? $\endgroup$
    – babou
    Commented Mar 6, 2014 at 21:31
  • $\begingroup$ @babou No, to be specific I was addressing the second part of the OP's post where he was talking about more general tools than straight translators from RuleML to Drools (e.g. Maude). The draft paper on the webpage linked to in my comment above also contains a large bibliography on similar tools to Lem and Maude in the introduction. $\endgroup$
    – Dominic Mulligan
    Commented Mar 7, 2014 at 9:32
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.