Table of Contents

I work at HPE on the Chapel Programming Language. Recently, another HPE person asked me:

So, you work on the programming language. What’s next for you?

This caught me off-guard because I hadn’t even conceived of moving on. I don’t want to move on, because I love the field of programming languages. In addition, I have come to think there is something in PL for everyone, from theorists to developers to laypeople. So, in that spirit, I am writing this list as a non-exhaustive survey that holds the dual purpose of explaining my personal infatuation with PL, and providing others with ways to engage with PL that align with their existing interests. I try to provide rationale for each claim, but you can just read the reasons themselves and skip the rest.

My general thesis goes something like this: programming languages are a unique mix of the inherently human and social and the deeply mathematical, a mix that often remains deeply grounded in the practical, low-level realities of our hardware.

Personally, I find all of these properties equally important, but we have to start somewhere. Let’s begin with the human aspect of programming languages.

Human Aspects of PL

Programs must be written for people to read, and only incidentally for machines to execute.

— Abelson & Sussman, Structure and Interpretation of Computer Programs.

As we learn more about the other creatures that inhabit our world, we discover that they are similar to us in ways that we didn’t expect. However, our language is unique to us. It gives us the ability to go far beyond the simple sharing of information: we communicate abstract concepts, social dynamics, stories. In my view, storytelling is our birthright more so than anything else.

I think this has always been reflected in the broader discipline of programming. Code should always tell a story, I’ve heard throughout my education and career. It should explain itself. In paradigms such as literate programming, we explicitly mix prose and code. Notebook technologies like Jupyter intersperse computation with explanations thereof.

From flowery prose to clinical report, human expression takes a wide variety of forms. The need to vary our descriptions is also well-served by the diversity of PL paradigms. From stateful transformations in languages like Python and C++, through pure and immutable functions in Haskell and Lean, to fully declarative statements-of-fact in Nix, various languages have evolved to support the many ways in which we wish to describe our world and our needs.

Those human thoughts of ours are not fundamentally grounded in logic, mathematics, or anything else. They are a product of millennia of evolution through natural selection, of adaptation to ever-changing conditions. Our cognition is limited, rife with blind spots, and partial to the subject matter at hand. We lean on objects, actors, contracts, and more as helpful, mammal-compatible analogies. I find this to be beautiful; here is something we can really call ours.

Storytelling (and, more generally, writing) is not just about communicating with others. Writing helps clarify one’s own thoughts, and to think deeper. In his 1979 Turing Award lecture, Notation as a Tool of Thought, Kenneth Iverson, the creator of APL, highlighted ways in which programming languages, with their notation, can help express patterns and facilitate thinking.

Throughout computing history, programming languages built abstractions that — together with advances in hardware — made it possible to create ever more complex software. Dijkstra’s structured programming crystallized the familiar patterns of if/else and while out of a sea of control flow. Structures and objects partitioned data and state into bundles that could be reasoned about, or put out of mind when irrelevant. Recently, I dare say that notions of ownership and lifetimes popularized by Rust have clarified how we think about memory.

The fight against complexity occurs on more battlegrounds than PL design alone. Besides its syntax and semantics, a programming language is comprised of its surrounding tooling: its interpreter or compiler, perhaps its package manager or even its editor. Language designers and developers take great care to improve the quality of error messages, to provide convenient editor tooling, and build powerful package managers like Yarn. Thus, in each language project, there is room for folks who, even if they are not particularly interested in grammars or semantics, care about the user experience.

I hope you agree, by this point, that programming languages are fundamentally tethered to the human. Like any human endeavor, then, they don’t exist in isolation. To speak a language, one usually wants a partner who understands and speaks that same language. Likely, one wants a whole community, topics to talk about, or even a set of shared beliefs or mythologies. This desire maps onto the realm of programming languages. When using a particular PL, you want to talk to others about your code, implement established design patterns, use existing libraries.

I mentioned mythologies earlier. In some ways, language communities do more than share know-how about writing code. In many cases, I think language communities rally around ideals embodied by their language. The most obvious example seems to be Rust. From what I’ve seen, the Rust community believes in language design that protects its users from the pitfalls of low-level programming. The Go community believes in radical simplicity. Julia actively incorporates contributions from diverse research projects into an interoperable set of scientific packages.

So far, I’ve presented interpretations of the field of PL as tools for expression and thought, human harbor to the universe’s ocean, and collaborative social projects. These interpretations coexist and superimpose, but they are only a fraction of the whole. What has kept me enamored with PL is that it blends these human aspects with a mathematical ground truth, through fundamental connections to computation and mathematics.

The Mathematics of PL

Like buses: you wait two thousand years for a definition of “effectively calculable”, and then three come along at once.

— Philip Wadler, Propositions as Types

There are two foundations, lambda calculus and Turing machines, that underpin most modern PLs. The abstract notion of Turing machines is closely related to, and most similar among the “famous” computational models, to the von Neumann Architecture. Through bottom-up organization of “control unit instructions” into “structured programs” into the imperative high-level languages today, we can trace the influence of Turing machines in C++, Python, Java, and many others. At the same time, and running on the same hardware functional programming languages like Haskell represent a chain of succession from the lambda calculus, embellished today with types and numerous other niceties. These two lineages are inseparably linked: they have been mathematically proven to be equivalent. They are two worlds coexisting.

The two foundations have a crucial property in common: they are descriptions of what can be computed. Both were developed initially as mathematical formalisms. They are rooted not only in pragmatic concerns of “what can I do with these transistors?”, but in the deeper questions of “what can be done with a computer?”.

Because of these mathematical beginnings, we have long had precise and powerful ways to talk about what code written in a particular language means. This is the domain of semantics. Instead of reference implementations of languages (CPython for Python, rustc for Rust), and instead of textual specifications, we can explicitly map constructs in languages either to mathematical objects (denotational semantics) or to (abstractly) execute them (operational semantics).

To be honest, the precise and mathematical nature of these tools is, for me, justification enough to love them. However, precise semantics for languages have real advantages. For one, they allow us to compare programs’ real behavior with what we expect, giving us a “ground truth” when trying to fix bugs or evolve the language. For another, they allow us to confidently make optimizations: if you can prove that a transformation won’t affect a program’s behavior, but make it faster, you can safely use it. Finally, the discipline of formalizing programming language semantics usually entails boiling them down to their most essential components. Stripping the syntax sugar helps clarify how complex combinations of features should behave together.

Some of these techniques bear a noticeable resemblance to the study of semantics in linguistics. Given our preceding discussion on the humanity of programming languages, perhaps that’s not too surprising.

In talking about how programs behave, we run into an important limitation of reasoning about Turing machines and lambda calculus, stated precisely in Rice’s theorem: all non-trivial semantic properties of programs (termination, throwing errors) are undecidable. There will always be programs that elude not only human analysis, but algorithmic understanding.

It is in the context of this constraint that I like to think about type systems. The beauty of type systems, to me, is in how they tame the impossible. Depending on the design of a type system, a well-typed program may well be guaranteed not to produce any errors, or produce only the “expected” sort of errors. By constructing reasonable approximations of program behavior, type systems allow us to verify that programs are well-behaved in spite of Rice’s theorem. Much of the time, too, we can do so in a way that is straightforward for humans to understand and machines to execute.

At first, type systems look like engineering formalisms. That may well be the original intention, but in our invention of type systems, we have actually completed a quadrant of a deeper connection: the Curry-Howard isomorphism. Propositions, in the logical sense, correspond one-to-one with types of programs, and proofs of these propositions correspond to programs that have the matching type.

This is an incredibly deep connection. In adding parametric polymorphism to a type system (think Java generics, or C++ templates without specialization), we augment the corresponding logic with the “for all x” (∀x\forall x) quantifier. Restrict the copying of values in a way similar to Rust, and you get an affine logic, capable of reasoning about resources and their use. In languages like Agda with dependent types, you get a system powerful enough to serve as a foundation for mathematics. Suddenly, you can write code and mathematically prove properties about that code in the same language. I’ve done this in my work with formally-verified static program analysis.

This connection proves appealing even from the perspective of “regular” mathematics. We have developed established engineering practices for writing code: review, deployment, documentation. What if we could use the same techniques for doing mathematics? What if, through the deep connection of programming languages to logic, we could turn mathematics into a computer-verified, collaborative endeavor? I therefore present:

Bonus meta-reason to love the mathy side of PL!

In addition to the theoretical depth, I also find great enjoyment in the way that PL is practiced. Here more than elsewhere, creativity and artfulness come into play. In PL, inference rules are a lingua franca through which the formalisms I’ve mentioned above are expressed and shared. They are such a central tool in the field that I’ve developed a system for exploring them interactively on this blog.

In me personally, inference rules spark joy. They are a concise and elegant way to do much of the formal heavy-lifting I described in this section; we use them for operational semantics, type systems, and sometimes more. When navigating the variety and complexity of the many languages and type systems out there, we can count on inference rules to take us directly to what we need to know. This same variety naturally demands flexibility in how rules are constructed, and what notation is used. Though this can sometimes be troublesome (one paper I’ve seen describes 27 different ways of writing the simple operation of substitution in literature!), it also creates opportunities for novel and elegant ways of formalizing PL.

  • Bonus Reason: the field of programming languages has a standard technique for expressing its formalisms, which precisely highlights core concepts and leaves room for creative expression and elegance.

I know that mathematics is a polarizing subject. Often, I find myself torn between wanting precision and eschewing overzealous formalism. The cusp between the two is probably determined by my own tolerance for abstraction. Regardless of how much abstraction you are interested in learning about, PL has another dimension, close to the ground: more often than not, our languages need to execute on real hardware.

Pragmatics of PL

Your perfectly-designed language can be completely useless if there is no way to [note: Technically, there are language that don't care if you execute them at all. Many programs in theorem-proving languages like Agda and Rocq exist only to be type-checked. So, you could nitpick this claim; or, you could take it more generally: your language can be useless if there's no way to make it efficiently do what it's been made to do. ] efficiently. Thus, the field of PL subsumes not only the theoretical foundations of languages and their human-centric design; it includes also their realization as software.

The overall point of this section is that there is much depth to the techniques involved in bringing a programming language to life. If you are a tinkerer or engineer at heart, you will never run out of avenues of exploration. The reasons are all framed from this perspective.

One fascinating aspect to programming languages is the “direction” from which they have grown. On one side, you have languages that came together from the need to control and describe hardware. I’d say that this is the case for C and C++, Fortran, and others. More often than not, these languages are compiled to machine code. Still subject to human constraints, these languages often evolve more user-facing features as time goes on. On the other side, you have languages developed to enable people to write software, later faced constraints of actually working efficiently. These are languages like Python, Ruby, and JavaScript. These languages are often interpreted (executed by a dedicated program), with techniques such as just-in-time compilation. There is no one-size-fits-all way to execute a language, and as a result,

At the same time, someone whose goal is to actually develop a compiler likely doesn’t want to develop everything from scratch. To do so would be a daunting task, especially if you want the compiler to run beyond the confines of a personal machine. CPU architectures and operating system differences are hard for any individual to keep up with. Fortunately, we have a gargantuan ongoing effort in the field: the LLVM Project. LLVM spans numerous architectures and targets, and has become a common back-end for languages like C++ (via Clang), Swift, and Rust. LLVM helps share and distribute the load of keeping up with the ongoing march of architectures and OSes. It also provides a shared playground upon which to experiment with language implementations, optimizations, and more.

Though LLVM is powerful, it does not automatically grant languages implemented with it good performance. In fact, no other tool does. To make a language run fast requires a deep understanding of the language itself, the hardware upon which it runs, and the tools used to execute it. That is a big ask! Modern computers are extraordinarily complex. Techniques such as out-of-order execution, caching, and speculative execution are constantly at play. This means that any program is subject to hard-to-predict and often unintuitive effects. On top of that, depending on your language’s capabilities, performance work can often entail working with additional hardware, such as GPUs and NICs, which have their own distinct performance characteristics. This applies both to compiled and interpreted languages. Therefore, I give you:

In the mathematics section, we talked about how constructing correct optimizations requires an understanding of the language’s semantics. It was one of the practical uses for having a mathematical definition of a language. Reason 13 is where that comes in, but the synthesis is not automatic. In fact, a discipline sits in-between defining how a language behaves and optimizing programs: program analysis. Algorithms that analyze properties of programs such as reaching definitions enable optimizations such as loop-invariant code motion, which can have very significant performance impact. At the same time, for an analysis to be correct, it must be grounded in the program’s mathematical semantics. There are many fascinating techniques in this discipline, including ones that use lattice theory.

The programs your compiler generates are software, and, as we just saw, may need to be tweaked for performance. But the compiler and/or interpreter is itself a piece of software, and its own performance. Today’s language implementations are subject to demands that hadn’t been there historically. For instance, languages are used to provide language servers to enable editors to give users deeper insights into their code. Today, a language implementation may be called upon every keystroke to provide a typing user live updates. This has led to the introduction of techniques like the query architecture (see also salsa) to avoid redundant work and re-used intermediate results. New language implementations like that of Carbon are exploring alternative representations of programs in memory. In short,

Conclusion

I’ve now given a tour of ways in which I found the PL field compelling, organized across three broad categories. There is just one more reason I’d like to share.

I was 16 years old when I got involved with the world of programming languages and compilers. Though I made efforts to learn about it through literature (the Dragon Book, and Modern Compiler Design), I simply didn’t have the background to find these resources accessible. However, all was not lost. The PL community online has been, and still is, a vibrant and enthusiastic place. I have found it to be welcoming of folks with backgrounds spanning complete beginners and experts alike. Back then, it gave me accessible introductions to anything I wanted. Now, every week I see new articles go by that challenge my intuitions, teach me new things, or take PL ideas to absurd and humorous extremes. So, my final reason: