Do some aggressive trimming and editing.

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

content/blog/i_love_programming_languages/index.md

@@ -0,0 +1,276 @@
+---
+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?
+
+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.
+
+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](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.
+
+* __Reason 1__: programming languages provide the foundation of expressing
+  human thought and stories through code.
+
+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.
+
+* __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.
+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.
+
+* __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/),
+and build powerful package managers
+like [Yarn](https://yarnpkg.com/). 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 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.
+
+* __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_
+
+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, 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?".
+
+* __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 (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.
+
+* __Reason 9__: in the face of the fundamentally impossible, type systems
+  grant us confidence in our programs for surprisingly little conceptual 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.
+In languages like Agda with [dependent types](https://en.wikipedia.org/wiki/Dependent_type),
+you get 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.
+
+{{< details summary="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, 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
+be troublesome (one [paper](https://labs.oracle.com/pls/apex/f?p=LABS%3A0%3A%3AAPPLICATION_PROCESS%3DGETDOC_INLINE%3A%3A%3ADOC_ID%3A959")
+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.
+{{< /details >}}