Harry R. Schwartz

Software engineer, nominal scientist, gentleman of the internet.
Member, ←Hotline Webring→.

bearded cartoon drawing of the author · 1B41 8F2C 23DE DD9C 807E A74F 841B 3DAE 25AE 721B

ovo-lacto vegetarian




Compilation as Search

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 related articles: