Podcasts about the Lean theorem prover

Using math to prove the correctness of computer programs, called formal methods, is perhaps the complete opposite of my usual interest in human–computer interaction. But they have fascinated me since my college years at Caltech, when I learned about them in my sophomore computer science class (a very unusual topic to cover at such an early stage). However, back then, you essentially had to prove the correctness of a program by hand, which was slow, tedious, and not practical. We played around with an early theorem prover, but it was clearly experimental.

So my interest was piqued when, thanks to an excerpt in Quanta Magazine, I learned about the book The Proof in the Code by Kevin Harnett, about the development of Lean, an interactive theorem prover that was originally targeted at proving the correctness of computer programs but has become the leading platform for formalizing mathematics. (OpenAI used Lean to verify its groundbreaking, and controversial, math proofs.) I’ve enjoyed the book so far, as it goes into the human stories behind Lean’s history.

But I wanted to learn more, so I’ve queued up a bunch of podcast episodes, mostly about Lean, but a few about other systems like TLA+ and formal methods in general. It’s almost 16 hours in total, and I’ve just started! In case you’re interested, here they are:

Updating Reason and ReScript in Wikipedia

A few years ago, I first learned of the Reason programming language, which is an alternate syntax to OCaml that more closely resembles JavaScript. Through a compiler called BuckleScript, Reason could also target JavaScript. But later, BuckleScript was rebranded as ReScript and introduced its own somewhat different syntax, essentially becoming its own programming language. It got very confusing for a while, but eventually everything settled down, and both projects are still going.

I was reminded of ReScript and Reason after listening to an episode of the excellent Developer Voices podcast (hosted by Kris Jenkins) about ReScript, so I started reading up on them again. That’s when I noticed that ReScript didn’t have its own Wikipedia article. So I created one.

I also noticed that the Wikipedia article on Reason was pretty outdated, so I updated it to reflect on how it has moved on to using another compiler for targeting JavaScript called Melange. (There was a great Developer Voices episode on Reason and Melange too.)

Hopefully, these changes will make the difference between Reason and ReScript more clear!

Stephanie Shirley, a pioneer in tech

I think my knowledge of computer history is decent, yet only now am I learning about Stephanie Shirley, a pioneer in the tech industry who started a software company in 1962 employing mostly women working part-time at home. Way ahead of her time 🫡

The Gorton Font

Marcin Wichary has done it again. He has written a wonderful essay on the Gorton font, a font you probably have never heard of but “probably saw earlier today.”

As I read it, I realized I had been noticing it my whole life subconsciously, and the words using it always felt important, since it was almost always engraved. If it’s engraved, it must be important, right?

Carol of the Bells in its original Ukrainian

This holiday season, I learned that the melody of the Christmas carol “Carol of the Bells” is from a Ukrainian New Year’s song called “Shchedryk” (Щедрик), first arranged in the early 1900s, which in turn is based on a traditional Ukrainian folk melody. Here is “Shchedryk” sung in its original Ukrainian:

Happy New Year everyone 🇺🇦

Handcrafted software in a mass-produced world

I’ve joked with my friends that I want to get into building hand-crafted, artisan software. Then Lian Proven of The Register makes the case for it, such as higher quality and being more attuned to a specific group’s needs.

I can think of a few examples of folks making hand-crafted software:

Bob James performs the theme song from Taxi

I’m a bit too young to have watched (or certainly understood) the sitcom Taxi, but I remember the opening theme song vividly. Here is Bob James, who wrote the song, performing it with his jazz trio at age 82. (Sometimes the YouTube algorithm is good for something!)

Yang Liping’s Rite of Spring

Last night, I watched Yang Liping’s interpretation of Stravinsky’s Rite of Spring at Stanford. Totally stunning and definitely worth watching. We also enjoyed her conversation with Thomas Mullaney (Stanford professor of history and East Asian languages and cultures) — like him, I didn’t fully understand what I saw 😂 but it set off my brain in all sorts of directions.

Here is a good overview of her work: