Harry R. Schwartz

Code writer, sometime Internet enthusiast, attractive nuisance.

The author at the Palais du Luxembourg in Paris, November 2022. hacker news gitlab sourcehut pinboard librarything 1B41 8F2C 23DE DD9C 807E A74F 841B 3DAE 25AE 721B


British Columbia



Compilation as Search


Published .
Tags: computer-science.

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.

Compilation as searching

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.

You might like these textually similar articles: