Programming Languages as
Objects in Nature🔗

In the early 1990s, the programming languages research community was in an optimistic mood. In the recent past, two of its paradigmatic languages—Scheme and ML—had formalized their semantics. For ML, it took the form of a whole book by Milner, et al. Scheme provided a denotational semantics in its standard. Surely, it seemed, it was only a matter of time before all languages went in this direction.

What went wrong?

If you’re a working programmer without a theoretical background, you might wonder why a formal semantics matters at all. It’s actually for reasons you can understand easily. When you write programs against code that someone else wrote, you like having an interface, or API, to program against. It mediates your conversation with the remote code, and anchors conversations about whom to blame if something doesn’t work as expected.
The formal semantics of a language does exactly the same thing. The language itself is the “remote code” you’re programming against. What it does should be pinned down as precisely as possible—but also as understandably as possible!—for you to work with.
The semantics isn’t just an interface for the user of a language. It’s also a crucial interface for tool authors, who must (also) otherwise guess at the behavior of the language. If you want an example of how even the relatively simple act of a variable rename refactoring can go wrong, see Appendix 2 of our Python semantics. A semantics doesn’t guarantee those kinds of errors won’t occur, but its absence makes them far more likely to.

For many researchers, it’s a given that programming languages are mathematical objects. This is a natural and attractive view. Languages are formal objects, after all; they are therefore amenable to codification by everything from logic to topology and more. (Formal) Specification is a natural consequence of this worldview.

The world, however, is full of programming languages that do not fit this model.Some may even have been created by programming language semanticists, which is worth pondering. Created by the ostensibly unwashed, they rudely announce their arrival with nothing more than an implementation. People pick them up, find them useful, do worthwhile things with them, and a million lines later, the next big “scripting language” is born. Let’s call these informal languages.

Informal languages are, of course, also amenable to formal specification. However, a crucial difference governs these two types of languages. Suppose we observe a difference between what the specification says and what the implementation does. In the case of Standard ML, for instance, one can approach the implementor, walk through the reasoning in the specification, and explain why the implementation is wrong. If the implementor agrees with your reasoning, no matter how unhappy this makes them, they must admit to and eventually fix their implementation.

The implementor of an informal language faces no such constraint. Faced with a mismatch between an ostensible specification and their implementation, they are free to simply laugh, question the specification’s parentage, and exit stage right. The specification can at best track what “the language is doing”, not really dictate its behavior.

Specification still serves a role. It can:

  • Shed light on what is happening inside a large and otherwise opaque implementation.

  • Point out complex designs that would warrant being simplified.

  • Highlight design aspects that are prone to cause programmer error, security violations, and so on.

  • Serve all the other uses of a specification, such as serving as a basis for building tools.

To do all these things usefully, however, the specification must take significant steps to show its conformance to the reality of the informal language, such as by running the same test suites as the implementations.

An informal language, then, is much more like an object found in nature:

A rock.

We can push at it, poke it, and prod it, and hope that it will yield its secrets. But we can never be certain—without the help of the implementors—that we have properly characterized all of it.

That doesn’t mean we can’t approach the problem systematically. Geologists, confronted with a rock, don’t flail helplessly. In high-school chemistry, I was taught to approach unknown substances with the SCODS test: check for its state, color, odor, density, and solubility.They never included a letter for “taste”, a reflection perhaps more of their aspiration than of the reality in a high school chemistry lab. That is, we identify some of dimensions of classification, and proceed along the principal axes.

We have these axes for programming languages, too. We can talk about their scope rules, their evaluation semantics, their type system, and so on. Indeed, because so much of a programmer’s career will be spent confronting informal languages and having to rapidly make sense out of them, I’ve long felt that how we teach programming languages should also be divided along these dimensions.

The problem of informal languages will not go away, so long as a dedicated amateur can scare up a new language’s implementation. Indeed, the size of our informal language space grows ever-bigger, and vastly so, than that of mathematical languages. In 2015, I made this slide:

Our programming stack.

It shows the stack atop which a typical client-side Web program of the day resided. What it actually shows is something much more subtle and important:

Programmers do not program in “languages”.

Rather, they program in some complex combination of languages, libraries, frameworks (which can impose their own operational behavior—e.g., seemingly turn a call-by-value language into a reactive one), and more. What a programmer needs is a semantics not just for the language sitting near the bottom, but rather for the mountain on top of which their program resides.

For illustrative examples of what such semantics might look like, see our work on the operational semantics of the DOM (it’s a giant control operator, y’all!), and the type structure of jQuery. But these are just a tiny sliver of a tiny sliver. How do we make real progress up the mountain and keep our position there as it keeps thrusting further out of the ground?

We can’t expect the date-picker library’s author to also be a semanticist. But we shouldn’t therefore resignedly conclude that we can never get there. Rather, we should acknowledge that there are useful divisions of labor. Instead of scolding informal language designers for their practices, semanticists need to find methods to bridge that gap, keeping in mind:

One can’t proceed from the informal to the formal by formal means.
—Alan Perlis

Whatever we propose needs to be:

  • Reasonable (in terms of skill) for the implementor to produce.

  • Useful for them to produce.

  • Useful for us to consume and work with.

One especially good intermediate proxy is a test suite of some sort. Tests don’t always get the respect they deserve, but they too are a form of specification. I like to call them “specifications from below”, precisely defining what should happen in individual cases, whereas the typical formal specification is “specification from above”, defining what happens across a family of cases. Ultimately, of course, we need specifications “from above”, but it’s worth noting that specifications “from below” are both useful to developers and something they are skilled at producing. The recent trend in languages of producing “confirmance suites” or “litmus tests” is especially promising in this regard. (Our work on formalizing the strict mode of of ECMAScript 5.1, for instance, made use of the ECMAScript conformance suite.)

How we use them remains a little bit of an open question. The most obvious use is to test our semantics: what Arjun Guha and I, to perhaps the horror of some, called a tested semantics. But we might also be able to generalize these tests, from “below” to “above”, i.e., it’s a synthesis problem. This requires some structure to produce a semantics that is also meaningful. Our paper on The Next 700 Semantics describes some of the contours for this line of work to consider.