technicalities: specs (Lisp, ML, ALGOL, Ada, JS2, ES4, RnRS, Redex, POPLmark, Rust, K, Comp/JSCert)
According to the History of Programming Languages website (currently offline) there have been somewhere around 8500 programming languages developed since the Autocodes of the early 50s. The internet archive has scraped HOPL's taxonomy at least as well as a few references and at least the primary year indexes (the year of my birth, for example).
It's an open secret among language designers that many, perhaps most languages in that set are not very well specified. To explain what this means and why it's so is ... a bit complicated. I will try to explain a little bit about it here, as well as some of my history with it and some recent innovations in the field that have been getting my attention.
To anyone uninterested in language design, this is super boring stuff, and this entry turned out to be much longer and involve much more wandering backstory than the previous one, so as usual I'll cut it for brevity.
When we build a programming language, we're creating a human-computer interface: a system of rules and relations with two very different "sides". On one side the rules define the set of all the programs a human is allowed to legally write in your language in a way that is meaningful to a human programmer and captures their intentions; and on the other side the rules define some mechanistic relationship between those legal programs and the sorts of computational actions and mathematical values -- input, output, reading and writing numbers in memory and so forth -- that have meaning inside a computer.
Artifacts
Language engineering, as a job, involves producing a set of artifacts that "specify" a coherent set of such rules and relationships. Unambiguously, completely, and in some sense practically: the artifacts need to be adequate for the human side -- people -- to write programs that work, and for the machine side -- interpreters and compilers -- to run those programs. Often we produce these multiple artifacts simultaneously, each of which captures some aspect of the job. Some examples:
Formalism and mechanization
When one of the artifacts in this list is present in a sufficiently formal form -- subject to an internal structure, logic and set of rules of its own -- it may itself be subject to mechanization by some program that implements the formalism: a meta-implementation. For example, when someone ships a formal grammar in the (A|E)BNF formalism, one of the advantages is that you can machine process it: analyze it, prove properties about it (say, complexity of parsing), and synthesize parsers for it using tools like YACC ("yet another compiler-compiler") or Bison (so named as a pun on YACC). This is super cool when it works, and is one of the strong motives for using formalisms in the first place: computers are good at helping us work with them.
Curiously, we often get close to using a formalism, but then stray. We may ship a "nearly" formal grammar, but not really tighten it up to the point of usability in production; we may choose to ship a "production" parser written by hand, rather than feeding a formal grammar through YACC, for reasons of comprehensibility, performance, error correction, diagnostic generation and so forth. As a case in point, it seems likely to me (despite my best efforts) that Rust may ship without a formal grammar. This is much more common than one might imagine.
Similar things happen with formal semantics. Often they're omitted entirely, but when they're written they're still often written in LaTeX! I.e. they're written for typesetting, for human readers; they're not mechanizable. This is partly because the mechanization tools lag behind the theory; it's also partly because the language-design process often proceeds informally and the formalization plays catch-up long after the production implementation has shipped (removing some of the advantage of mechanization -- you don't need to synthesize a slow interpreter from the spec if you already have a production compiler). Partly it's also due to simple cognitive load: there's only so much mental budget available and learning formalisms and the mechanizations thereof is quite a chore in itself. Often it's just not considered to pay for itself, especially in industry. Academia is often more patient, and they tend to develop tidier, better-studied languages. Industrial languages are more often "specified" with english-plus-an-RI, and seldom with any formal semantics.
Languages like, say, PHP or Perl are at an extreme end of this spectrum. Nobody even pretends they have a formal semantics, much less a mechanizable one; Perl5 mostly even lacks a formal grammar. The RI is the strongest component of the spec. On the other end there are things like the Lisps and MLs, which actually grew out of the implementation layers for formal reasoning tools in the late 50s and early 70s respectively, and often have very well-studied, well-formalized semantics, and well-studied reference implementations. The descendants of these formal reasoning tools live on more powerful and general modern incarnations like Coq, HOL, Isabelle, Twelf, ACL2 and (as I mentioned earlier) Maude.
Ancient history
This tension has been with us as long as people have been specifying languages. Consider ALGOL (initially IAL, the "International Algebraic Language", SO CUTE), the first language to ever seek the status of an international standard. ALGOL is old enough that BNF was actually invented to specify it, for formalizing the grammar in ALGOL60. Consider the infamous later revision, ALGOL68, which attempted to specify more of the language using a more-powerful, undecidable formalism (W-grammars, a sort of attribute-grammar then in vogue): this variant was mostly considered "too complicated to understand", and tools to work with the spec were beyond the familiarity of most implementers. Simplifications that unwound the cognitive load of the spec back to BNF-and-english followed.
By contrast, consider that in 1975 the US DoD design process that resulted in Ada did not attempt any fancier-than-BNF formalisms. The requirement documents (STRAWMAN, WOODENMAN, TINMAN,IRONMAN and STEELMAN); the candidate language specs (Red, Green, Blue, Yellow and Tartan); and the final winner Green which became Ada, were all BNF-and-english. Academic tools -- and many were being developed! -- didn't really figure into the process. The only STEELMAN requirement that reads on this at all is To the extent that a formal definition assists in achieving the above goals (i.e., all of section 1), the language shall be formally defined.
In practice no additional formalisms came into play, and the informal english bits just kept growing (indeed, the Tartan proposal was an academic response to what was perceived as runaway complexity in the informal process). It's worth studying the resulting documents. They're quite brute-force, but also highly comprehensive, understandable. One can probably program in Ada as confidently as in Standard ML, despite the fact that the informal definition of the former is as much as 10 times larger than the formal definition of the latter, and there's no mechanization in sight.
More recent and personal history
Anyway, that's all backstory from before I was born! Fast forward through a few decades of people struggling with this tension, specifying languages and maturing tools, while I learned to tie my shoes and ride bikes. By 2006 I was working in industry and starting to get involved in language design, having spent a while working on other people's languages. I joined Mozilla in order to work on a language-spec-in-progress called ES4 ("EcmaScript 4", a.k.a. the trademarked "JavaScript"). ES4 never shipped, for reasons I'm not going to get much into here, but along the way we struggled a fair bit with the tension between formalisms and informality. Curiously, ES4 was actually a sort of "reboot" of an earlier Netscape language-design process called JavaScript 2, which was highly formalized! It was an executable formal semantics written in Common Lisp, by Waldemar Horwat. (Extra-curiously, I interviewed to work with Waldemar on this language back in 1999, but that's another story).
Part of the language-design context in 2006-8 was an academic competition called the POPLmark challenge, a set of successively harder-to-mechanize tasks in formal language specification that had several viable entries from the communities of researchers around Coq, HOL, Twelf and the like. Since I saw this going on and was very green and optimistic, and knew that the JS2 effort had been highly formalism-friendly, I tried to push for doing ES4 in a mechanized logical framework. The committee -- sympathetic but much more experienced and dubious -- pushed back and we settled on a (terrible) compromise of doing our RI in ML, with some modules normative and some informative. At least that would be higher-level and easier to work with than the "english pseudocode" that made up the ES3 spec, and might rest on better formal foundations. This was a mistake, but it's all over now. ES4 died, ES5 succeeded and ES6 is on the way.
Around the same time as ES4, another language called Scheme (a very well-studied Lisp) was undergoing its 6th revision: R6RS. Some of the folks working on ES4 were following R6RS closely, and I vaguely remember we entertained a guest expert from that community. The scheme community pushed hard on formalization in that round, using a tool from the PLT group called Redex. Redex is a very domain-specific tool, not a general logical framework; it's aimed squarely at the needs of language designers, and in practice this seems to make the barrier to entry much lower. Perhaps as evidence: the resulting R6RS spec did actually ship with an executable Redex model.
The present day
Subsequently, as I mentioned above, I've spent quite some time working on Rust. We stayed on the less-formal side while developing it, favoring english and a solid RI (perhaps I was a bit burned by ES4). I worry of course that it should have more formal parts, but having stepped away from it I'm kinda resigned to an observer status; this post is not about trying to influence its direction, it's more a retrospective and context post, pointing out some tools and projects I think are currently interesting. Redex is definitely one of them, and I was excited to see both Lindsey working on an initial Redex model, and later Niko developing one of his own. I don't know what will actually ship, but it's an encouraging sign that in 2014 industrial systems languages at least consider this a plausible step.
Parallel to my interest in Redex, I've of course been fiddling around with Maude (mentioned in an earlier post), and have noticed a tool similar in spirit to Redex emerge out of the Maude community. This is called the K Framework, and seems quite focused on providing domain-specific tools to language engineers. It has, in its short life, chalked up some pretty impressive mechanized (executable) models: reasonably complete semantics for Scheme, Python and C, as well as some work-in-progress semantics of other production systems (JVM, LLVM, Haskell).
Finally, mechanized specification in Coq has not stood still! The community received a bit of a jolt in 2008 when Xavier Leroy, Sandrine Blazy and their team released CompCert, a Coq formalization of C, and PowerPC machines, and a reference implementation compiler that translates between the two, with mechanized proofs of correctness. Following on the heels of this, a project called JSCert just released a Coq formalization of ES5 (the version of EcmaScript that came after the ES4 process collapsed). Like CompCert, this includes both spec and RI, as well as proof of correctness relative to spec.
So it's exciting times! The gulf between formal (and mechanized-formal) and informal appears to be, if not exactly dissolving, at least beginning to thaw. Industrial languages in production are beginning to see realistic, end-to-end mechanized specification for the first time, if not during development then at least "shortly thereafter". I don't know exactly when the tide will turn permanently, but it seems likely within the next few generations of languages.
This entry was originally posted at http://graydon2.dreamwidth.org/1839.html. Please comment there using OpenID.
It's an open secret among language designers that many, perhaps most languages in that set are not very well specified. To explain what this means and why it's so is ... a bit complicated. I will try to explain a little bit about it here, as well as some of my history with it and some recent innovations in the field that have been getting my attention.
To anyone uninterested in language design, this is super boring stuff, and this entry turned out to be much longer and involve much more wandering backstory than the previous one, so as usual I'll cut it for brevity.
When we build a programming language, we're creating a human-computer interface: a system of rules and relations with two very different "sides". On one side the rules define the set of all the programs a human is allowed to legally write in your language in a way that is meaningful to a human programmer and captures their intentions; and on the other side the rules define some mechanistic relationship between those legal programs and the sorts of computational actions and mathematical values -- input, output, reading and writing numbers in memory and so forth -- that have meaning inside a computer.
Artifacts
Language engineering, as a job, involves producing a set of artifacts that "specify" a coherent set of such rules and relationships. Unambiguously, completely, and in some sense practically: the artifacts need to be adequate for the human side -- people -- to write programs that work, and for the machine side -- interpreters and compilers -- to run those programs. Often we produce these multiple artifacts simultaneously, each of which captures some aspect of the job. Some examples:
- A spec document in a natural language like english, sometimes in bullet-point form or with all-caps words like MUST and SHALL at the very important parts.
- A formal grammar written in some formal grammar-specifying language, like ABNF.
- A formal semantics, typically of the type system and evaluation model, written in the logic rules of some semantic framework like operational or denotational semantics.
- A reference implementation (RI) -- an interpreter or compiler -- written in some executable language.
- A conformance testsuite -- a set of programs -- that's expected to work, accompanied by expected results.
- Ill-specifying: describing a language that either doesn't make sense -- contains internal contradictions -- or that causes programs written in it to themselves be systematically flawed (unsafe, erroneous).
- Underspecifying: not providing enough detail, so people can't determine if the language is ill-specified, and/or they can't they tell which programs are valid, or what they mean.
- Overspecifying: providing too much detail, so people have too many details to check for ill-specificity / bugs, and/or are too constrained in how they implement the language (needless idiosyncrasies).
Formalism and mechanization
When one of the artifacts in this list is present in a sufficiently formal form -- subject to an internal structure, logic and set of rules of its own -- it may itself be subject to mechanization by some program that implements the formalism: a meta-implementation. For example, when someone ships a formal grammar in the (A|E)BNF formalism, one of the advantages is that you can machine process it: analyze it, prove properties about it (say, complexity of parsing), and synthesize parsers for it using tools like YACC ("yet another compiler-compiler") or Bison (so named as a pun on YACC). This is super cool when it works, and is one of the strong motives for using formalisms in the first place: computers are good at helping us work with them.
Curiously, we often get close to using a formalism, but then stray. We may ship a "nearly" formal grammar, but not really tighten it up to the point of usability in production; we may choose to ship a "production" parser written by hand, rather than feeding a formal grammar through YACC, for reasons of comprehensibility, performance, error correction, diagnostic generation and so forth. As a case in point, it seems likely to me (despite my best efforts) that Rust may ship without a formal grammar. This is much more common than one might imagine.
Similar things happen with formal semantics. Often they're omitted entirely, but when they're written they're still often written in LaTeX! I.e. they're written for typesetting, for human readers; they're not mechanizable. This is partly because the mechanization tools lag behind the theory; it's also partly because the language-design process often proceeds informally and the formalization plays catch-up long after the production implementation has shipped (removing some of the advantage of mechanization -- you don't need to synthesize a slow interpreter from the spec if you already have a production compiler). Partly it's also due to simple cognitive load: there's only so much mental budget available and learning formalisms and the mechanizations thereof is quite a chore in itself. Often it's just not considered to pay for itself, especially in industry. Academia is often more patient, and they tend to develop tidier, better-studied languages. Industrial languages are more often "specified" with english-plus-an-RI, and seldom with any formal semantics.
Languages like, say, PHP or Perl are at an extreme end of this spectrum. Nobody even pretends they have a formal semantics, much less a mechanizable one; Perl5 mostly even lacks a formal grammar. The RI is the strongest component of the spec. On the other end there are things like the Lisps and MLs, which actually grew out of the implementation layers for formal reasoning tools in the late 50s and early 70s respectively, and often have very well-studied, well-formalized semantics, and well-studied reference implementations. The descendants of these formal reasoning tools live on more powerful and general modern incarnations like Coq, HOL, Isabelle, Twelf, ACL2 and (as I mentioned earlier) Maude.
Ancient history
This tension has been with us as long as people have been specifying languages. Consider ALGOL (initially IAL, the "International Algebraic Language", SO CUTE), the first language to ever seek the status of an international standard. ALGOL is old enough that BNF was actually invented to specify it, for formalizing the grammar in ALGOL60. Consider the infamous later revision, ALGOL68, which attempted to specify more of the language using a more-powerful, undecidable formalism (W-grammars, a sort of attribute-grammar then in vogue): this variant was mostly considered "too complicated to understand", and tools to work with the spec were beyond the familiarity of most implementers. Simplifications that unwound the cognitive load of the spec back to BNF-and-english followed.
By contrast, consider that in 1975 the US DoD design process that resulted in Ada did not attempt any fancier-than-BNF formalisms. The requirement documents (STRAWMAN, WOODENMAN, TINMAN,IRONMAN and STEELMAN); the candidate language specs (Red, Green, Blue, Yellow and Tartan); and the final winner Green which became Ada, were all BNF-and-english. Academic tools -- and many were being developed! -- didn't really figure into the process. The only STEELMAN requirement that reads on this at all is To the extent that a formal definition assists in achieving the above goals (i.e., all of section 1), the language shall be formally defined.
In practice no additional formalisms came into play, and the informal english bits just kept growing (indeed, the Tartan proposal was an academic response to what was perceived as runaway complexity in the informal process). It's worth studying the resulting documents. They're quite brute-force, but also highly comprehensive, understandable. One can probably program in Ada as confidently as in Standard ML, despite the fact that the informal definition of the former is as much as 10 times larger than the formal definition of the latter, and there's no mechanization in sight.
More recent and personal history
Anyway, that's all backstory from before I was born! Fast forward through a few decades of people struggling with this tension, specifying languages and maturing tools, while I learned to tie my shoes and ride bikes. By 2006 I was working in industry and starting to get involved in language design, having spent a while working on other people's languages. I joined Mozilla in order to work on a language-spec-in-progress called ES4 ("EcmaScript 4", a.k.a. the trademarked "JavaScript"). ES4 never shipped, for reasons I'm not going to get much into here, but along the way we struggled a fair bit with the tension between formalisms and informality. Curiously, ES4 was actually a sort of "reboot" of an earlier Netscape language-design process called JavaScript 2, which was highly formalized! It was an executable formal semantics written in Common Lisp, by Waldemar Horwat. (Extra-curiously, I interviewed to work with Waldemar on this language back in 1999, but that's another story).
Part of the language-design context in 2006-8 was an academic competition called the POPLmark challenge, a set of successively harder-to-mechanize tasks in formal language specification that had several viable entries from the communities of researchers around Coq, HOL, Twelf and the like. Since I saw this going on and was very green and optimistic, and knew that the JS2 effort had been highly formalism-friendly, I tried to push for doing ES4 in a mechanized logical framework. The committee -- sympathetic but much more experienced and dubious -- pushed back and we settled on a (terrible) compromise of doing our RI in ML, with some modules normative and some informative. At least that would be higher-level and easier to work with than the "english pseudocode" that made up the ES3 spec, and might rest on better formal foundations. This was a mistake, but it's all over now. ES4 died, ES5 succeeded and ES6 is on the way.
Around the same time as ES4, another language called Scheme (a very well-studied Lisp) was undergoing its 6th revision: R6RS. Some of the folks working on ES4 were following R6RS closely, and I vaguely remember we entertained a guest expert from that community. The scheme community pushed hard on formalization in that round, using a tool from the PLT group called Redex. Redex is a very domain-specific tool, not a general logical framework; it's aimed squarely at the needs of language designers, and in practice this seems to make the barrier to entry much lower. Perhaps as evidence: the resulting R6RS spec did actually ship with an executable Redex model.
The present day
Subsequently, as I mentioned above, I've spent quite some time working on Rust. We stayed on the less-formal side while developing it, favoring english and a solid RI (perhaps I was a bit burned by ES4). I worry of course that it should have more formal parts, but having stepped away from it I'm kinda resigned to an observer status; this post is not about trying to influence its direction, it's more a retrospective and context post, pointing out some tools and projects I think are currently interesting. Redex is definitely one of them, and I was excited to see both Lindsey working on an initial Redex model, and later Niko developing one of his own. I don't know what will actually ship, but it's an encouraging sign that in 2014 industrial systems languages at least consider this a plausible step.
Parallel to my interest in Redex, I've of course been fiddling around with Maude (mentioned in an earlier post), and have noticed a tool similar in spirit to Redex emerge out of the Maude community. This is called the K Framework, and seems quite focused on providing domain-specific tools to language engineers. It has, in its short life, chalked up some pretty impressive mechanized (executable) models: reasonably complete semantics for Scheme, Python and C, as well as some work-in-progress semantics of other production systems (JVM, LLVM, Haskell).
Finally, mechanized specification in Coq has not stood still! The community received a bit of a jolt in 2008 when Xavier Leroy, Sandrine Blazy and their team released CompCert, a Coq formalization of C, and PowerPC machines, and a reference implementation compiler that translates between the two, with mechanized proofs of correctness. Following on the heels of this, a project called JSCert just released a Coq formalization of ES5 (the version of EcmaScript that came after the ES4 process collapsed). Like CompCert, this includes both spec and RI, as well as proof of correctness relative to spec.
So it's exciting times! The gulf between formal (and mechanized-formal) and informal appears to be, if not exactly dissolving, at least beginning to thaw. Industrial languages in production are beginning to see realistic, end-to-end mechanized specification for the first time, if not during development then at least "shortly thereafter". I don't know exactly when the tide will turn permanently, but it seems likely within the next few generations of languages.
This entry was originally posted at http://graydon2.dreamwidth.org/1839.html. Please comment there using OpenID.