Church's λ-Calculus (2023) [pdf]

I've got Harper's Practical Foundations for Programming Languages and it's a great book—he writes clearly and succinctly.

Knowing the lambda calculus helped me one time when I was working as a software engineer: I had just added functions to a little DSL interpreter that was going to make it easy to customize behavior of our product to different customers. (It wasn't ever going to be used by customers directly; it was primarily a tool for the internal team.) It was at this point that I realized we needed some kind of execution time-out: since we could encode functions, we could write down e.g. the Y combinator or the omega combinator and we could get non-terminating programs in this DSL.

Now I work as a programming languages researcher, so the lambda calculus has direct application to my day job.

Those curious might be interested in ISWIM, [1,2] which is an extension of the lambda calculus with an arbitrary set of operators. Like the lambda calculus, this is an abstract language. However, you can add numbers and other operators, and ISWIM-like languages are often used to illustrate new ideas in programming languages.

Syntax is incidental. Boil the syntax away from languages and reduce them to their distilled semantics to get out the essential differences—this is the kind of thing that the lambda calculus makes easy.

I highly recommend reading Landin's The Next 700 Programming Languages [2] as it is a great, short, clear read.

[1]: https://en.wikipedia.org/wiki/ISWIM [2]: https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf

There has to be some programmer rite of passage involving learning lambda calculus. I went through this a few years ago when something similar was posted. I learned the notation, marveled at its dual simplicity and completeness, and and did a few exercises. But I came out the other side none the wiser. I think I was looking for some great epiphany on the nature of computation. Alas, it eluded me in the end. It was fun but ultimately useless for me.

I love theory, and I also really like lambda calculus, but I feel like this sentiment applies to most theory, particularly stuff after undergrad.

I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and...

Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it.

And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely.

It was enough to depress me, and it still kind of does.

I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.

I work on web-adjacent-shit, mostly data processing stuff in Kafka that eventually ends up on the web.

I don't get to recurse over JSON, occasionally I get to design a system from scratch and that's more fun, but it's usually not more complicated than "draw boxes that point to other boxes and/or cylinders on screen". Sometimes I draw a picture of cloud.

I like my job just fine, it's a decent job, and I like my managers and coworkers as well, but it's just disappointing that enthusiasm for math and theory is what got me to this stage of my career, but I never really got to use it, and I don't see that ever really changing for me.

Maybe I will write a paper at some point at least.

I use the deep theory experience a ton when designing software or systems. But I don't do an actual proof hardly ever. Being able to reason about a problem and intuit the extent of what's technologically possible to solve is insanely useful. But in most places that I work everyone around me can do that too, so we're constantly battling program managers and C suite guys / gals who just don't see why everything is so slow, difficult, un-scalable, unpredictable, etc. They want a stupid thing that works half the time, and they'll just turn the camera off the other half of the time.