<p>We have been working on one for the last few years: <a href="http://www.cl.cam.ac.uk/~pes20/lem/" rel="nofollow">Lem</a>, 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.</p>

CC BY-SA 3.0
2014-03-06T21:31:37.257Z
Have you attempted the kind of translation from one language to another envisioned by the OP?
babou
CC BY-SA 3.0
2014-03-07T09:32:24.123Z
@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.
Dominic Mulligan
CC BY-SA 3.0
2014-03-06T15:11:38.987Z
2014-03-06T15:11:38.987Z
Dominic Mulligan
<p>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 <a href="https://en.wikipedia.org/wiki/Structure_editor" rel="nofollow">structured editors</a> 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. <a href="http://compcert.inria.fr/doc/" rel="nofollow">Coq has been used for that</a> and it is still on-going work.</p>

<p>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.</p>

<p>It is true that some systems based on <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">Curry-Howard isomorphism</a> and <a href="https://en.wikipedia.org/wiki/Intuitionistic_type_theory" rel="nofollow">type theory</a>, such as <a href="https://en.wikipedia.org/wiki/Coq" rel="nofollow">Coq</a>, 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.</p>

<p>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.</p>

CC BY-SA 3.0
2014-03-06T00:10:07.870Z
2014-03-06T07:59:39.543Z
2014-03-06T07:59:39.543Z
babou
<p>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. </p>

<p>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.</p>

<p>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.</p>

<fl.formal-languages><pl.programming-languages><semantics><operational-semantics>
Tool for specifying operational semantics for given formally specified programming language
TomR
# Tool for specifying operational semantics for given formally specified programming language

(Asked by: username_0 on 2014-03-05)

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.

**Tags:** fl.formal-languages, pl.programming-languages, semantics, operational-semantics


---

## 2 answers

### Answer by username_1 on 2014-03-06. Score: 3

We have been working on one for the last few years: [Lem](http://www.cl.cam.ac.uk/~pes20/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.

> **Comments:**
> **username_2**: Have you attempted the kind of translation from one language to another envisioned by the OP?  
> **username_1**: @username_2 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.  

---

### Answer by username_2 on 2014-03-06. Score: 1

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](https://en.wikipedia.org/wiki/Structure_editor) 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](http://compcert.inria.fr/doc/) 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](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) and [type theory](https://en.wikipedia.org/wiki/Intuitionistic_type_theory), such as [Coq](https://en.wikipedia.org/wiki/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.


---

