This short paper by Russ Cox exemplifies everything I believe about theory. It takes a tool that programmers use all the time—regular expressions, which are the basis of search and replace—and shows how the standard implementation of them can fail badly at many tasks. It then walks through some basic computer science theory to derive a different implementation of regular expressions, one that performs well all the time.
This is a theoretical pearl: the mathematics are simple, well-understood, and provably correct. But it’s also profoundly practical: once you write out the theory carefully, the program follows as a matter of course. The formalism is the program. Sadly, people who ought to know better still get this one wrong.
I write law review articles and legal documents now, rather than programs and computer science papers. But the lesson is the same. Good theory is useful.
For more information, here’s Russ’s overview page, and here’s his follow-up with equally elegant implementation details. I had the pleasure of working with him years ago; he’s also an all-round nice guy and the only Free Electron I know.