Machine readable specifications

Andreas Rossberg rossberg at
Fri Mar 22 06:23:16 PDT 2013

On 22 March 2013 13:37, gaz Heyes <gazheyes at> wrote:
> On 22 March 2013 12:33, Andreas Rossberg <rossberg at> wrote:
>> Aren't you confusing "machine readable specification" with "machine
>> readable syntax specification"? Syntax is only a small part of a
>> language spec, and quite frankly, the least interesting one by far.
>> Also, I don't see the benefit of your format. The EcmaScript spec
>> actually goes to quite some length to give a grammar that is LR(1).
>> The whole point is to keep it de facto "machine readable". But unlike
>> yours, it also is human readable.
> That was the reason to discuss, I think it could be applied to more than
> just syntax rules. You don't like it and that's fine with me I just wanted
> to post my ideas.

You may be underestimating the challenge ;). If you are aiming for
more than just syntax then you certainly wouldn't want a low-level
encoding like the one you suggest. The standard approach to
formalising a language is through a structured operational semantics
over an abstract syntax, and the standard approach to making that
accessible to a machine is encoding it in an established theorem
prover or language like Coq or Isabelle or Agda or Twelf.


More information about the es-discuss mailing list