Halfspace

Subscribe
Archives
August 17, 2025

The same colored grass

Recently Dan Abramov, an experienced software engineer who does a lot of frontend development, has been learning real analysis via lean and posting his thoughts alongside other developers.

His take take on the textbook definition of real numbers, which is essentially "mind blown," made me smile because of how tedious the same ideas are framed by most mathematicians. I can't help but recall Michael Spivak's canonical textbook Calculus, which not only defers the definition of real numbers until the last chapter, but starts that chapter with, "The mass of drudgery which this chapter necessarily contains..." Instead Abramov says his experience (and particularly lean+Mathlib) feels like "Minecraft for rigorous thought."

As I read this I was reminded of a flipped situation. In 2021 the category theorist Emily Riehl gave a talk at Google, "An Introduction to Homotopy Type Theory and Univalent Foundations." Toward the end of that talk she described what she loved about the field, and while I can't quote her from memory, it was something like, "the proofs are beautiful because you get so much for free from the types." This struck me because, of course types give you a lot for free! This is the basis of so much of programming language design and software engineering practice.

My initial reaction to this kind of situation in isolation is usually somewhere between XKCD's Ten Thousand and "how cute." Like watching an undergraduate math student who just realized why the limit definition of the derivative makes sense and is elegant.

But having both of their expressions of joy in view at the same time, it strikes me just how much each doesn't realize how much joy their side is providing to the other. Programmers take their type systems for granted, and even grumble loudly about them, while mathematicians may bear the type system as mental overhead for their entire careers. On the other hand, mathematicians often treat axiomatic foundations, like the Dedekind cuts of the real numbers or Euclid's geometry, as something to be done once and forgotten, perhaps not even realizing how many people still have their minds blown from these old ideas. (James Propp does a great job of remembering the joy in his monthly, history-focused essays.)

I don't have a name for this idea, that someone who fell in love with an art or trade later forgets how it initially made them feel, but it must surely be an old concept. It's something like "the grass is always greener on the other side of the fence," but where there's no fence and you just start noticing the weeds between the grass more than the brilliant color because you see the same grass every day.

At the very least, this is a reminder to me to keep engaging with newcomers. They can rekindle our joy vicariously, and that's worth much more than the time required to help them. And when you do find some joy, share it.

Don't miss what's next. Subscribe to Halfspace:
Powered by Buttondown, the easiest way to start and grow your newsletter.