Do some aggressive trimming and editing.

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

content/blog/i_love_programming_languages/index.md

@@ -11,28 +11,18 @@ 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.
+This caught me off-guard because I hadn't even conceived of moving on.
-Next? From this? Upon some reflection, I realized that I hadn't even imagined
+I don't want to move on, because __I love the field of programming languages__.
-worlds in which I voluntarily do anything other than working on programming
+In addition, I have come to think there is something in PL for everyone, from
-languages. Upon further reflection, I realized just how deeply __I love the
+theorists to developers to laypeople.
-field__. The part that surprised me the most was to realize just how varied
+So, in that spirit, I am writing this list as a non-exhaustive survey that holds
-the things I find appealing are; the more I think about it, the more I become
+the dual purpose of explaining my personal infatuation with PL, and providing
-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
+our hardware__.
-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.
@@ -45,8 +35,7 @@ start somewhere. Let's begin with the human aspect of programming languages.
 > --- 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
+that they are similar to us in ways that we didn't expect. However, our
-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
@@ -57,22 +46,17 @@ _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
+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
+From flowery prose to clinical report, human expression takes a wide variety
-there are many ways to tell a story. From flowery prose to clinical report,
+of forms. The need to vary our descriptions is also well-served by the diversity
-human expression takes a wide variety of forms. The need to vary
+of PL paradigms. From stateful transformations in languages like Python and C++,
-our descriptions is also well-served by the diversity of PL paradigms.
+through pure and immutable functions in Haskell and Lean, to fully declarative
-From stateful transformations in languages like Python and C++, through
+statements-of-fact in Nix, various languages have evolved to
-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
@@ -82,13 +66,10 @@ 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.
-If we were pure, logical agents, we could write our code in the stripped-down
+Our cognition is limited, rife with blind spots, and partial to the subject
-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,
+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
@@ -120,12 +101,11 @@ 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/)
+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
+and build powerful package managers
-like [Yarn](https://yarnpkg.com/), [`uv`](https://docs.astral.sh/uv/),
+like [Yarn](https://yarnpkg.com/). Thus, in each language project, there is
-and more. Thus, in each language project, there is room for folks who,
+room for folks who, even if they are not particularly interested in grammars or
-even if they are not particularly interested in grammars or semantics, care
+semantics, care about the user experience.
-about the user experience.
 
 * __Reason 5__: programming languages provide numerous opportunities for
   thoughtful forays into the realms of User Experience and Human-Computer
@@ -145,11 +125,9 @@ 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
+from the pitfalls of low-level programming. The Go community
-believes in radical simplicity, rejecting the never-ending layering of
+believes in radical simplicity. Julia actively incorporates contributions from
-abstractions in language design. Julia incorporates numeric representations and
+diverse research projects into an interoperable set of scientific packages.
-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
@@ -169,12 +147,6 @@ computation and mathematics.
 >
 > --- 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
@@ -185,11 +157,11 @@ to the
 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
+At the same time, and running on the same hardware functional programming
-than one might expect, functional programming languages like Haskell represent
+languages like Haskell represent a chain of succession from the lambda calculus,
-a chain of succession from the lambda calculus, embellished today with
+embellished today with types and numerous other niceties. These two lineages
-types and numerous other niceties. These two lineages are inseparably linked:
+are inseparably linked: they have been mathematically proven to be equivalent.
-they have been mathematically proven to be equivalent. Two lives doing the same thing.
+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.
@@ -230,25 +202,21 @@ 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](https://en.wikipedia.org/wiki/Rice%27s_theorem):
-all non-trivial semantic properties of programs are undecidable. This means
+all non-trivial semantic properties of programs (termination, throwing errors)
-that in general, we can't decide for certain whether a program terminates
+are undecidable. There will always be programs that elude not only human analysis,
-or runs infinitely (see the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)),
+but algorithmic understanding.
-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
+Depending on the design of a type system, a well-typed program may well be
-produce only the "expected" sort of errors, or or terminate. Though the precise
+guaranteed not to produce any errors, or produce only the "expected" sort of
-properties guaranteed by any given type system vary by language or even by
+errors. By constructing reasonable _approximations_ of program
-type checker, the general principle holds: by constructing reasonable
+behavior, type systems allow us to verify that programs are well-behaved in
-_approximations_ of program behavior, type systems allow us to verify that
+spite of Rice's theorem. Much of the time, too, we can do so in a way that is
-programs are well-behaved in spite of Rice's theorem. Much of the time, too,
+straightforward for humans to understand and machines to execute.
-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.
+  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,
@@ -262,9 +230,9 @@ 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
+[affine logic](https://en.wikipedia.org/wiki/Affine_logic), capable of reasoning about resources and their use.
-[dependent types](https://en.wikipedia.org/wiki/Dependent_type), like in Idris, and you
+In languages like Agda with [dependent types](https://en.wikipedia.org/wiki/Dependent_type),
-have a system powerful enough [to serve as a foundation for mathematics](https://en.wikipedia.org/wiki/Intuitionistic_type_theory).
+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" >}}).
@@ -281,7 +249,7 @@ I therefore present:
   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
@@ -297,14 +265,12 @@ 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," >}}
+be troublesome (one [paper](https://labs.oracle.com/pls/apex/f?p=LABS%3A0%3A%3AAPPLICATION_PROCESS%3DGETDOC_INLINE%3A%3A%3ADOC_ID%3A959")
-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 __27__ different ways of writing the simple operation of substitution in literature!),
-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
+* __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 >}}