[WIP] 2/3 draft

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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 <a href="https://labs.oracle.com/pls/apex/f?p=LABS%3A0%3A%3AAPPLICATION_PROCESS%3DGETDOC_INLINE%3A%3A%3ADOC_ID%3A959">paper</a>
+I've seen describes <em class="bold">27</em> 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.