The other day I went to see Faré’s talk at Boston Haskell on first-class implementations. I thought it was terrific, though a lot of it was over my head.

I latched onto a particular throwaway reference that he made midway through the talk. He mentioned that if a bit of code has a semantic meaning, or intent, then compilation is the process of searching through the space of possible programs in the target language for ones that share that same meaning.

That’s slick! I’ve always thought of compilation as automated translation, but turning it around into a search problem feels like a novel way of thinking about it (at least, novel to me—I’m sure there’s a paper from the ’60s that lays this whole idea out, but I haven’t come across it yet).

This also reminds me of some of the ideas in Wadler’s Propositions as Types: under this framing our initial program represents the proof of a theorem in one logical system, and compilation is the search for another proof of the same theorem using a different logic.

Anyway, this feels like it’s probably a lot of woo, but it’s interesting woo.