diff --git a/content/blog/i_love_programming_languages/cardeli-products.png b/content/blog/i_love_programming_languages/cardeli-products.png new file mode 100644 index 0000000..ce51ee4 Binary files /dev/null and b/content/blog/i_love_programming_languages/cardeli-products.png differ diff --git a/content/blog/i_love_programming_languages/index.md b/content/blog/i_love_programming_languages/index.md new file mode 100644 index 0000000..705a16c --- /dev/null +++ b/content/blog/i_love_programming_languages/index.md @@ -0,0 +1,310 @@ +--- +title: "Reasons to Love the Field of Programming Languages" +date: 2025-12-06T18:08:24-08:00 +draft: true +tags: ["Programming Languages", "Compilers", "Type Systems"] +--- + +I work at HPE on the +[Chapel Programming Language](https://chapel-lang.org). Recently, another HPE +person asked me: + +> So, you work on the programming language. What's next for you? + +The question caught me so off-guard that I had to make sure I heard it right. +Next? From this? Upon some reflection, I realized that I hadn't even imagined +worlds in which I voluntarily do anything other than working on programming +languages. Upon further reflection, I realized just how deeply __I love the +field__. The part that surprised me the most was to realize just how varied +the things I find appealing are; the more I think about it, the more I become +convinced that +{{< sidenote "right" "pl-note" "programming languages" >}} +I will hereafter abbreviate this as PL to save probably kilobytes of storage +space for this post. +{{< /sidenote >}} +has something to offer a lot of people. So, in that spirit, I thought I'd +write up the variety of reasons I love PL, to share my enthusiasm. This +list is a non-exhaustive survey that holds the dual purpose +of explaining my personal infatuation with the field, and providing +others with ways to engage with PL that align with their existing interests. + +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__. In these many domains, PL rewards creativity and encourages +artfulness. + +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. They conceive +of time, have internal lives, individual identities. 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](https://en.wikipedia.org/wiki/Literate_programming), +we explicitly mix prose and code. Notebook technologies +like [JuPyTer](https://jupyter.org/) intersperse computation with explanations +thereof. + +Viewing programming as a more precise form of storytelling, I can give the +first reason I love PL: + +* __Reason 1__: programming languages provide the foundation of expressing + human thought and stories through code. + +This begs a follow-up. There are many ways to think about a problem, and +there are many ways to tell a story. 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 Prolog and Nix, various languages have evolved to +support the many ways in which we wish to describe our world and our needs. + +* __Reason 2__: diverse programming languages enable different perspectives + and ways of storytelling, allowing us choice in how to express our thoughts + and solve our problems. + +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. +If we were pure, logical agents, we could write our code in the stripped-down +and pure frameworks of +[lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) or +[Turing machines](https://en.wikipedia.org/wiki/Turing_machine). Instead, +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. Thus, + +* __Reason 3__: programming languages imbue the universe's fundamental rules of + computation with humanity's identity and idiosyncrasies. They carve out + a home for us within impersonal reality. + +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](https://www.eecg.utoronto.ca/~jzhu/csc326/readings/iverson.pdf), +Kenneth Iverson, the creator of [APL](https://tryapl.org/), 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](https://en.wikipedia.org/wiki/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. + +* __Reason 4__: programming languages combat complexity, and give us tools to + think and reason about unwieldy and difficult problems. + +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](https://elm-lang.org/news/compiler-errors-for-humans), +to provide [convenient editor tooling](https://chapel-lang.org/blog/posts/chapel-lsp/) +(hey, that's us on the Chapel team!), and build powerful package managers +like [Yarn](https://yarnpkg.com/), [`uv`](https://docs.astral.sh/uv/), +and more. 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. + +* __Reason 5__: programming languages provide numerous opportunities for + thoughtful forays into the realms of User Experience and Human-Computer + Interaction. + +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 precarious landscape of low-level programming. The Go community +believes in radical simplicity, rejecting the never-ending layering of +abstractions in language design. Julia incorporates numeric representations and +algorithms from diverse research projects into an interoperable collection +of scientific packages. + +* __Reason 6__: programming languages are complex collaborative social projects + that have the power to champion innovative ideas within the field of + computer science. + +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_ + +Imagine for a moment that along the familiar carbon-based, DNA-carrying +life, there existed on Earth life built from entirely different building +blocks. It would look and act pretty much the same, but somehow be made +at its core from different _stuff_. This is how I feel about the mathematical +underpinnings of practical programming languages. + +There are two foundations, +[lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) and +[Turing machines](https://en.wikipedia.org/wiki/Turing_machine), 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](https://en.wikipedia.org/wiki/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, running on the same hardware and looking more familiar +than one might expect, 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. Two lives doing the same thing. + +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?". + +* __Reason 7__: programming languages are built on foundations of computation, + and wield the power to compute anything we consider "effectively computable at all". + +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](https://en.wikipedia.org/wiki/Denotational_semantics)) +or to (abstractly) execute them ([operational semantics](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Syntactic_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. + +* __Reason 8__: programming languages can be precisely formalized, giving + exact, mathematical descriptions of how they should work. + +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](https://en.wikipedia.org/wiki/Rice%27s_theorem): +all non-trivial semantic properties of programs are undecidable. This means +that in general, we can't decide for certain whether a program terminates +or runs infinitely (see the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)), +or if it throws exceptions / produces errors. 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. +A well-typed program may well be guaranteed not to produce any errors, or +produce only the "expected" sort of errors, or or terminate. Though the precise +properties guaranteed by any given type system vary by language or even by +type checker, the general principle holds: 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. + +* __Reason 9__: in the face of the fundamentally impossible, type systems + grant us confidence in our programs for surprisingly little cost. + +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](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). +[Propositions](https://en.wikipedia.org/wiki/Proposition), 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" (\(\forall x\)) quantifier. +Restrict the copying of values in a way similar to Rust, and you get an +[affine logic](https://en.wikipedia.org/wiki/Affine_logic), capable of reasoning about resources and their use. Add +[dependent types](https://en.wikipedia.org/wiki/Dependent_type), like in Idris, and you +have a system powerful enough [to serve as a foundation for mathematics](https://en.wikipedia.org/wiki/Intuitionistic_type_theory). +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]({{< relref "series/static-program-analysis-in-agda" >}}). + +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: + +* __Reason 10__: type systems for programming languages deeply correspond + to logic, allowing us to mathematically prove properties about code, + using code, and to advance mathematics through the practices of software engineering. + + +In addition to the theoretical depth, I also find great enjoyment in the way that PL is practiced. +Here more than elsewhere, the creativity and artfulness I've mentioned before come into +play. In PL, [inference rules](https://en.wikipedia.org/wiki/Rule_of_inference) 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]({{< relref "blog/bergamot" >}}) +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 +{{< sidenote "right" "notation-note" "be troublesome," >}} +One paper +I've seen describes 27 different ways +of writing the simple operation of substitution. +{{< /sidenote >}} +it also creates opportunities for novel and elegant ways of formalizing +PL. + +* __Reason 11__: 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.