<p>How would one formally define a programming language?</p>
<p>What are the ways in which one can think about how to communicate a programming language design?</p>
<p>What languages and frameworks exist with which to define and describe programming languages?</p>
<p>Are there different layers of abstraction and/or categories to consider?</p>
<p>I've heard of <a href="https://kframework.org/" rel="noreferrer">K</a>, which seems relevant and am wondering what alternatives there are and how they relate:</p>
<blockquote>
<p>K is a rewrite-based executable semantic framework in which
programming languages, type systems and formal analysis tools can be
defined using configurations and rules.</p>
</blockquote>

<k-framework><semantics>
How might one formally communicate/define/describe a programming language design?
CC BY-SA 4.0
2023-05-16T17:34:28.527Z
What is this question asking? Do you want to know how to formally define a programming language?
Ginger
CC BY-SA 4.0
2023-05-16T17:37:37.473Z
Yes, updated; it's a broad question and might get some interesting answers I hope!
Lee
<p>Generally, programming languages are modeled using specialized mathematical notation for humans, and/or in <a href="https://en.wikipedia.org/wiki/Formal_methods" rel="noreferrer"><strong>formal methods</strong></a> languages like K and also <a href="https://coq.inria.fr/" rel="noreferrer">Coq</a> and <a href="https://docs.racket-lang.org/redex/" rel="noreferrer">Redex</a> for computers. An example of the human notation is on page 7 of <a href="https://dl.acm.org/doi/pdf/10.1145/3453483.3454039" rel="noreferrer">Retrofitting Effect Handlers in OCaml</a>, which defines the full operational semantics of multicore OCaml effect handlers. An example of the computer approach is in <a href="https://compcert.org/" rel="noreferrer">CompCert</a>, a formally-verified C compiler: the team modeled the complete behavior of C and Assembly in Coq, including writing a C AST and assembly interpreter, and then the Coq proof checker used this model to prove that their compiler was behavior-preserving (the interpreted AST of any valid program has the same behavior as the compiled version).</p>
<p>Technically, a language's syntax and semantics are &quot;defined&quot; by its parser and interpreter/compiler, which is the ground truth, but there are many systems invented to better convey this information so it can be understood by humans and reasoned about by computers:</p>
<ul>
<li><strong>Syntax:</strong> Via <a href="https://en.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_form" rel="noreferrer">EBNF</a>, <a href="https://en.wikipedia.org/wiki/Augmented_Backus%E2%80%93Naur_form" rel="noreferrer">ABNF</a>, and <a href="https://en.wikipedia.org/wiki/Metasyntax#Specific_metasyntax_conventions" rel="noreferrer">other</a> <a href="http://www.cs.man.ac.uk/%7Epjj/bnf/ebnf.html" rel="noreferrer">notations</a></li>
<li><strong>Semantics:</strong> <a href="https://en.wikipedia.org/wiki/Operational_semantics" rel="noreferrer">Operational semantics</a> (<a href="https://en.wikipedia.org/wiki/Operational_semantics#Small-step_semantics" rel="noreferrer">small-step</a> and <a href="https://en.wikipedia.org/wiki/Operational_semantics#Big-step_semantics" rel="noreferrer">big-step</a>), <a href="https://en.wikipedia.org/wiki/Denotational_semantics" rel="noreferrer">denotational semantics</a>, <a href="https://en.wikipedia.org/wiki/Evaluation_strategy" rel="noreferrer">evaluation strategy</a>, <a href="https://en.wikipedia.org/wiki/Typing_rule" rel="noreferrer">typing rules</a>, etc.</li>
</ul>
<p>When describing a programming language and in particular its <em>design</em>, eventually you veer into informal territory. For example, usually syntactic sugar is completely invisible to the compiler, and certain constructs like <code>do while</code> loops, <code>while</code> loops, <code>for</code> loops, will be collapsed into a single representation (loops). These details aren't important for the formal definition (not very important to the computers), but some of them are very important to humans. Therefore, it's still best to describe some parts of your language informally in plain English, like:</p>
<ul>
<li>Is there a static or dynamic type system?</li>
<li>Is memory management implicit or explicit?</li>
<li>What's in its standard library?</li>
<li>What are the coding conventions?</li>
<li>How easy is the language to learn? Which languages will it be easier to transition from?</li>
</ul>

CC BY-SA 4.0
2023-05-16T20:03:06.393Z
2023-05-16T20:03:06.393Z
tarzh
CC BY-SA 4.0
2023-05-17T08:47:07.827Z
I love this answer; I wonder if a language's ground truth syntax and semantics must also include a description of the machine upon which the interpreted/compiled code runs?
Lee
CC BY-SA 4.0
2023-05-17T16:18:37.753Z
Technically yes, but fortunately most machines run the exact same code with the exact same behavior (barring speed, which isn't considered behavior anyways)
tarzh
CC BY-SA 4.0
2023-05-17T16:19:29.007Z
And factors like disk size, other files, etc. aren't considered part of the program's behavior
tarzh
<p>In conference papers, the usual way is:</p>
<ul>
<li>Extended BNF definition for the syntax, with textual description of some non-core features.</li>
<li>Using inference rules (usually in the style of natural deduction) to describe the typing rules.</li>
<li>Use induction on syntax or rewrite rules to define the operational semantics.</li>
</ul>
<p>Example:</p>
<ul>
<li>Syntax: <code>a, b, c ::= a + b | a &gt; b | a ? b : c</code></li>
<li>Textual description of non-core features: &quot;we'll be using parentheses for precedences&quot;</li>
<li>Inference rules (one example):
<pre><code>a : bool  b : τ  c : τ
----------------------
     (a ? b : c) : τ
</code></pre>
</li>
<li>Operational semantics (one example):
<pre><code>true ? b : c ---&gt; b
false ? b : c ---&gt; c
</code></pre>
</li>
</ul>
<p>The K framework provides a general framework for operational semantics with rewrite rules.</p>
<p>On the other hand, there is <a href="https://www.metaborg.org/en/latest" rel="nofollow noreferrer">spoofax</a>, which provides a datalog-style framework for typing rules.</p>

CC BY-SA 4.0
2023-05-16T17:38:52.453Z
2023-09-04T22:10:02.217Z
2023-09-04T22:10:02.217Z
ice1000
<p>For completeness I must mention the C++ ISO standard.</p>
<p>While it doesn't include mathematic proofs like some answers.
It does include:</p>
<ul>
<li>complete syntax</li>
<li>very precise wording indicating how each language construct should behave whilst allowing for implementation specific / undefined behaviour.</li>
</ul>
<p>Basically there are several compatible ways:</p>
<ul>
<li>syntax</li>
<li>academic papers</li>
<li>mathematical proofs relating to the type system and such like</li>
<li>documentation thoroughly describing the language</li>
<li>a reference implementation</li>
</ul>

CC BY-SA 4.0
2023-05-28T14:11:30.600Z
2023-05-29T17:17:33.467Z
2023-05-29T17:17:33.467Z
Bruce Adams
<p>There is the <a href="https://smlfamily.github.io/sml97-defn.pdf" rel="noreferrer">definition of Standard ML</a> using operational semantics for its typechecking (&quot;static semantics&quot;) and evaluation (&quot;dynamic semantics&quot;), which has been <a href="https://github.com/SMLFamily/The-Mechanization-of-Standard-ML" rel="noreferrer">formalized</a> with <a href="http://twelf.org/wiki/Main_Page" rel="noreferrer">Twelf</a>.</p>

CC BY-SA 4.0
2023-05-16T17:39:30.270Z
2023-05-16T17:39:30.270Z
Alex Nelson
CC BY-SA 4.0
2023-05-16T20:07:44.480Z
A more recent (and more wide-spread) programming language with the same approach for specification is [WebAssembly](https://webassembly.github.io/spec/), which also has its typing and reduction defined in terms of inference rules, complemented with a reference interpreter and a formalizations in [Isabelle](https://github.com/WasmCert/WasmCert-Isabelle) and [Coq](https://github.com/WasmCert/WasmCert-Coq).
Matija Pretnar
CC BY-SA 4.0
2023-05-17T14:09:42.503Z
@MatijaPretnar Excellent, excellent! It's wonderful to hear about WebAssembly, I didn't know it was formalized to such degree. My focus has been on functional languages, like Standard ML, which sadly lack analogous modern results (besides [CakeML](https://cakeml.org/)) :(
Alex Nelson
CC BY-SA 4.0
2023-09-07T06:45:30.627Z
With regards to WebAssembly: they do some *very* interesting stuff around formal semantics, having [a DSL](https://github.com/Wasm-DSL/spectec) for generating the typing rules, formal proofs, interpreter, *and* prose.
apropos
<p>In practise, and despite most of the other answers, essentially <strong>the only way</strong> a mainstream, real world programming language <span class="math-container">$L$</span> is defined, is by building a <span class="math-container">$L$</span>-compiler that translates to, or an <span class="math-container">$L$</span>-interpreter that executes in another programming language (typically a machine language), which is assumed to be understood.</p>
<p>The  others suggestion (like K, or natural deduction rules) are used for small toy languages, but not for mainstream, real world programming languages, such as C, C++, Haskell, Agda, Lean, Python etc. That's because the effort of fully defining the syntax and semantics of a mainstream PL is so heroic that one doesn't want to do it more than once. And where it is done more than once (e.g.  clang and gcc) the results don't coincide ...</p>
<p>The reason why the other methods are used and very useful is essentially <em>divide-and-conquer</em>: we sketch the essence of computation mechanisms in toy calculi (e.g. <span class="math-container">$\lambda$</span>-calculus for <span class="math-container">$\beta$</span>-reduction, and <span class="math-container">$\pi$</span>-calculus for message passing parallelism, or Datalog for proof search, ...), and ignore handling  of various other problems (e.g. finiteness of numbers) because that would obscure the phenomenon we are trying to handle, and leave it to another toy model. The full, real-world compiler then 'only' has to solve  of brining all those many different issues together in one unified whole. A good example here is ML, where Robin Milner separated out the presentation of type-inference into separate papers (e.g. L. Damas, R. Milner, <em>Principal type-schemes for functional programs</em>) which do not explain type inference for full ML, but only a toy model of it, a small λ-calculus. I think this is a good approach: compiler / interpreter + small calculi to exhibit novel ideas in the language.</p>

CC BY-SA 4.0
2023-09-06T06:55:27.117Z
2023-09-07T08:10:10.340Z
2023-09-07T08:10:10.340Z
Martin Berger
CC BY-SA 4.0
2023-09-06T07:04:10.043Z
While it's true that most languages don't have any formal communication, definition, or description, this doesn't seem to address the question of *how one might do those things*.
Michael Homer
CC BY-SA 4.0
2023-09-06T07:04:44.760Z
@MichaelHomer I'd argue that you can always start by writing an interpreter ... That is in fact what I usually do.
Martin Berger
<blockquote>
<p>What languages and frameworks exist with which to define and describe programming languages?</p>
</blockquote>
<p>English is one such language.</p>
<p>Natural languages like English can absolutely be used for formal communication. The <a href="https://docs.oracle.com/javase/specs/jls/se19/html/" rel="nofollow noreferrer">Java Language Specification</a> is written in formal technical English, with a bit of mathematical notation mixed in where necessary.</p>
<p>For a taste, here's an excerpt from <a href="https://docs.oracle.com/javase/specs/jls/se19/html/jls-15.html#jls-15.12.2.5" rel="nofollow noreferrer">§15.12.2.5. Choosing the Most Specific Method</a>: I've added bold formatting to highlight technical terms which are defined elsewhere in the JLS. (I've highlighted only the first use of each term.)</p>
<blockquote>
<p>One <strong>applicable method</strong> <span class="math-container">$m_1$</span> is <em>more specific</em> than another applicable method <span class="math-container">$m_2$</span>, for an <strong>invocation</strong> with <strong>argument</strong> <strong>expressions</strong> <span class="math-container">$e_1, \ldots, e_k$</span>, if any of the following are true:</p>
<ul>
<li><p><span class="math-container">$m_2$</span> is <strong>generic</strong>, and <span class="math-container">$m_1$</span> is inferred to be <em>more specific</em> than <span class="math-container">$m_2$</span> for argument expressions <span class="math-container">$e_1, \ldots, e_k$</span> by §18.5.4.</p>
</li>
<li><p><span class="math-container">$m_2$</span> is not generic, and <span class="math-container">$m_1$</span> and <span class="math-container">$m_2$</span> are applicable by <strong>strict</strong> or <strong>loose invocation</strong>, and where <span class="math-container">$m_1$</span> has <strong>formal parameter types</strong> <span class="math-container">$S_1, \ldots, S_n$</span> and <span class="math-container">$m_2$</span> has formal parameter types <span class="math-container">$T_1, \ldots, T_n$</span>, the <strong>type</strong> <span class="math-container">$S_i$</span> is <strong><em>more specific</em></strong> than <span class="math-container">$T_i$</span> for argument <span class="math-container">$e_i$</span> for all <span class="math-container">$i$</span> (<span class="math-container">$1 \le i \le n$</span>, <span class="math-container">$n = k$</span>).</p>
</li>
<li><p><span class="math-container">$m_2$</span> is not generic, and <span class="math-container">$m_1$</span> and <span class="math-container">$m_2$</span> are applicable by <strong>variable arity invocation</strong>, and where the first <span class="math-container">$k$</span> <strong>variable arity parameter types</strong> of <span class="math-container">$m_1$</span> are <span class="math-container">$S_1, \ldots, S_k$</span> and the first <span class="math-container">$k$</span> variable arity parameter types of <span class="math-container">$m_2$</span> are <span class="math-container">$T_1, \ldots, T_k$</span>, the type <span class="math-container">$S_i$</span> is <em>more specific</em> than <span class="math-container">$T_i$</span> for argument <span class="math-container">$e_i$</span> for all <span class="math-container">$i$</span> (<span class="math-container">$1 \le i \le k$</span>). Additionally, if <span class="math-container">$m_2$</span> has <span class="math-container">$k+1$</span> <strong>parameters</strong>, then the <span class="math-container">$k+1$</span>'th variable arity parameter type of <span class="math-container">$m_1$</span> is a <strong>subtype</strong> of the <span class="math-container">$k+1$</span>'th variable arity parameter type of <span class="math-container">$m_2$</span>.</p>
</li>
</ul>
</blockquote>
<p>It's very dense, but (as I've hopefully shown) every term used has a defined, specific meaning. Perhaps being in English, it is more likely to contain mistakes than if it were written in a formal language that could be verified; nonetheless, the JLS certainly communicates, defines and describes a programming language.</p>

CC BY-SA 4.0
2023-09-06T21:12:38.133Z
2023-09-06T21:12:38.133Z
kaya3
# How might one formally communicate/define/describe a programming language design?
Posted by: username_0 on 2023-05-16
How would one formally define a programming language?

What are the ways in which one can think about how to communicate a programming language design?

What languages and frameworks exist with which to define and describe programming languages?

Are there different layers of abstraction and/or categories to consider?

I've heard of [K](https://kframework.org/), which seems relevant and am wondering what alternatives there are and how they relate:

> K is a rewrite-based executable semantic framework in which
> programming languages, type systems and formal analysis tools can be
> defined using configurations and rules.
**Tags:** k-framework semantics
> **Comments:**
> **username_1**: What is this question asking? Do you want to know how to formally define a programming language?  
> **username_0**: Yes, updated; it's a broad question and might get some interesting answers I hope!  
---
## 6 answers
### Answer by username_2 on 2023-05-16. Score: 9
Generally, programming languages are modeled using specialized mathematical notation for humans, and/or in [**formal methods**](https://en.wikipedia.org/wiki/Formal_methods) languages like K and also [Coq](https://coq.inria.fr/) and [Redex](https://docs.racket-lang.org/redex/) for computers. An example of the human notation is on page 7 of [Retrofitting Effect Handlers in OCaml](https://dl.acm.org/doi/pdf/10.1145/3453483.3454039), which defines the full operational semantics of multicore OCaml effect handlers. An example of the computer approach is in [CompCert](https://compcert.org/), a formally-verified C compiler: the team modeled the complete behavior of C and Assembly in Coq, including writing a C AST and assembly interpreter, and then the Coq proof checker used this model to prove that their compiler was behavior-preserving (the interpreted AST of any valid program has the same behavior as the compiled version).

Technically, a language's syntax and semantics are "defined" by its parser and interpreter/compiler, which is the ground truth, but there are many systems invented to better convey this information so it can be understood by humans and reasoned about by computers:

* **Syntax:** Via [EBNF](https://en.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_form), [ABNF](https://en.wikipedia.org/wiki/Augmented_Backus%E2%80%93Naur_form), and [other](https://en.wikipedia.org/wiki/Metasyntax#Specific_metasyntax_conventions) [notations](http://www.cs.man.ac.uk/%7Epjj/bnf/ebnf.html)
* **Semantics:** [Operational semantics](https://en.wikipedia.org/wiki/Operational_semantics) ([small-step](https://en.wikipedia.org/wiki/Operational_semantics#Small-step_semantics) and [big-step](https://en.wikipedia.org/wiki/Operational_semantics#Big-step_semantics)), [denotational semantics](https://en.wikipedia.org/wiki/Denotational_semantics), [evaluation strategy](https://en.wikipedia.org/wiki/Evaluation_strategy), [typing rules](https://en.wikipedia.org/wiki/Typing_rule), etc.

When describing a programming language and in particular its *design*, eventually you veer into informal territory. For example, usually syntactic sugar is completely invisible to the compiler, and certain constructs like `do while` loops, `while` loops, `for` loops, will be collapsed into a single representation (loops). These details aren't important for the formal definition (not very important to the computers), but some of them are very important to humans. Therefore, it's still best to describe some parts of your language informally in plain English, like:

* Is there a static or dynamic type system?
* Is memory management implicit or explicit?
* What's in its standard library?
* What are the coding conventions?
* How easy is the language to learn? Which languages will it be easier to transition from?
> **Comments:**
> **username_0** (2023-05-17): I love this answer; I wonder if a language's ground truth syntax and semantics must also include a description of the machine upon which the interpreted/compiled code runs?  
> **username_2** (2023-05-17): Technically yes, but fortunately most machines run the exact same code with the exact same behavior (barring speed, which isn't considered behavior anyways)  
> **username_2** (2023-05-17): And factors like disk size, other files, etc. aren't considered part of the program's behavior  
---
### Answer by username_3 on 2023-05-16. Score: 9
In conference papers, the usual way is:

Extended BNF definition for the syntax, with textual description of some non-core features.
Using inference rules (usually in the style of natural deduction) to describe the typing rules.
Use induction on syntax or rewrite rules to define the operational semantics.

Example:

Syntax: a, b, c ::= a + b | a > b | a ? b : c
Textual description of non-core features: "we'll be using parentheses for precedences"
Inference rules (one example):
a : bool  b : τ  c : τ
----------------------
     (a ? b : c) : τ


Operational semantics (one example):
true ? b : c ---> b
false ? b : c ---> c



The K framework provides a general framework for operational semantics with rewrite rules.
On the other hand, there is spoofax, which provides a datalog-style framework for typing rules.
---
### Answer by username_5 on 2023-05-16. Score: 7
There is the [definition of Standard ML](https://smlfamily.github.io/sml97-defn.pdf) using operational semantics for its typechecking ("static semantics") and evaluation ("dynamic semantics"), which has been [formalized](https://github.com/SMLFamily/The-Mechanization-of-Standard-ML) with [Twelf](http://twelf.org/wiki/Main_Page).
> **Comments:**
> **username_6** (2023-05-16): A more recent (and more wide-spread) programming language with the same approach for specification is [WebAssembly](https://webassembly.github.io/spec/), which also has its typing and reduction defined in terms of inference rules, complemented with a reference interpreter and a formalizations in [Isabelle](https://github.com/WasmCert/WasmCert-Isabelle) and [Coq](https://github.com/WasmCert/WasmCert-Coq).  
> **username_5** (2023-05-17): @MatijaPretnar Excellent, excellent! It's wonderful to hear about WebAssembly, I didn't know it was formalized to such degree. My focus has been on functional languages, like Standard ML, which sadly lack analogous modern results (besides [CakeML](https://cakeml.org/)) :(  
> **username_7** (2023-09-07): With regards to WebAssembly: they do some *very* interesting stuff around formal semantics, having [a DSL](https://github.com/Wasm-DSL/spectec) for generating the typing rules, formal proofs, interpreter, *and* prose.  
---
### Answer by username_4 on 2023-05-28. Score: 4
For completeness I must mention the C++ ISO standard.

While it doesn't include mathematic proofs like some answers.
It does include:

* complete syntax
* very precise wording indicating how each language construct should behave whilst allowing for implementation specific / undefined behaviour.

Basically there are several compatible ways:

* syntax
* academic papers
* mathematical proofs relating to the type system and such like
* documentation thoroughly describing the language
* a reference implementation
---
### Answer by username_10 on 2023-09-06. Score: 3
> What languages and frameworks exist with which to define and describe programming languages?

English is one such language.

Natural languages like English can absolutely be used for formal communication. The [Java Language Specification](https://docs.oracle.com/javase/specs/jls/se19/html/) is written in formal technical English, with a bit of mathematical notation mixed in where necessary.

For a taste, here's an excerpt from [§15.12.2.5. Choosing the Most Specific Method](https://docs.oracle.com/javase/specs/jls/se19/html/jls-15.html#jls-15.12.2.5): I've added bold formatting to highlight technical terms which are defined elsewhere in the JLS. (I've highlighted only the first use of each term.)

> One **applicable method** $m\_1$ is *more specific* than another applicable method $m\_2$, for an **invocation** with **argument** **expressions** $e\_1, \ldots, e\_k$, if any of the following are true:
>
> * $m\_2$ is **generic**, and $m\_1$ is inferred to be *more specific* than $m\_2$ for argument expressions $e\_1, \ldots, e\_k$ by §18.5.4.
> * $m\_2$ is not generic, and $m\_1$ and $m\_2$ are applicable by **strict** or **loose invocation**, and where $m\_1$ has **formal parameter types** $S\_1, \ldots, S\_n$ and $m\_2$ has formal parameter types $T\_1, \ldots, T\_n$, the **type** $S\_i$ is ***more specific*** than $T\_i$ for argument $e\_i$ for all $i$ ($1 \le i \le n$, $n = k$).
> * $m\_2$ is not generic, and $m\_1$ and $m\_2$ are applicable by **variable arity invocation**, and where the first $k$ **variable arity parameter types** of $m\_1$ are $S\_1, \ldots, S\_k$ and the first $k$ variable arity parameter types of $m\_2$ are $T\_1, \ldots, T\_k$, the type $S\_i$ is *more specific* than $T\_i$ for argument $e\_i$ for all $i$ ($1 \le i \le k$). Additionally, if $m\_2$ has $k+1$ **parameters**, then the $k+1$'th variable arity parameter type of $m\_1$ is a **subtype** of the $k+1$'th variable arity parameter type of $m\_2$.

It's very dense, but (as I've hopefully shown) every term used has a defined, specific meaning. Perhaps being in English, it is more likely to contain mistakes than if it were written in a formal language that could be verified; nonetheless, the JLS certainly communicates, defines and describes a programming language.
---
### Answer by username_8 on 2023-09-06. Score: 2
In practise, and despite most of the other answers, essentially **the only way** a mainstream, real world programming language $L$ is defined, is by building a $L$-compiler that translates to, or an $L$-interpreter that executes in another programming language (typically a machine language), which is assumed to be understood.

The others suggestion (like K, or natural deduction rules) are used for small toy languages, but not for mainstream, real world programming languages, such as C, C++, Haskell, Agda, Lean, Python etc. That's because the effort of fully defining the syntax and semantics of a mainstream PL is so heroic that one doesn't want to do it more than once. And where it is done more than once (e.g. clang and gcc) the results don't coincide ...

The reason why the other methods are used and very useful is essentially *divide-and-conquer*: we sketch the essence of computation mechanisms in toy calculi (e.g. $\lambda$-calculus for $\beta$-reduction, and $\pi$-calculus for message passing parallelism, or Datalog for proof search, ...), and ignore handling of various other problems (e.g. finiteness of numbers) because that would obscure the phenomenon we are trying to handle, and leave it to another toy model. The full, real-world compiler then 'only' has to solve of brining all those many different issues together in one unified whole. A good example here is ML, where Robin Milner separated out the presentation of type-inference into separate papers (e.g. L. Damas, R. Milner, *Principal type-schemes for functional programs*) which do not explain type inference for full ML, but only a toy model of it, a small λ-calculus. I think this is a good approach: compiler / interpreter + small calculi to exhibit novel ideas in the language.
> **Comments:**
> **username_9** (2023-09-06): While it's true that most languages don't have any formal communication, definition, or description, this doesn't seem to address the question of *how one might do those things*.  
> **username_8** (2023-09-06): @MichaelHomer I'd argue that you can always start by writing an interpreter ... That is in fact what I usually do.  
---
