ezyang’s blog

the arc of software bends towards understanding

Computer Science

“This is really the End.”

Done. This adjective rarely describes any sort of software project—there are always more bugs to fix, more features to add. But on September 20th, early one afternoon in France, Georges Gonthier did just that: he slotted in the last component of a six year project, with the laconic commit message, "This is really the End." […]

  • September 24, 2012

Why verification results in higher quality code

Correctness is overrated. After all, no one knows what it means for any reasonably complicated system to be "correct", and even when we do, the mileposts move around on a daily basis. With the raison d'être of formal verification stripped away, can we still consider it a worthy goal? Perhaps verification results in higher quality […]

  • June 23, 2012

What happens when you mix three research programming languages together

“...so that’s what we’re going to build!” “Cool! What language are you going to write it in?” “Well, we were thinking we were going to need three programming languages...” “...three?” “...and they’ll be research programming languages too...” “Are you out of your mind?” This was the conversation in streaming through my head when I decided […]

  • May 16, 2012

Some thoughts about literature review

While working on my senior thesis, I had to write a prior work section, which ended up being a minisurvey for the particular subfield my topic was in. In the process, a little bird told me some things... If you can, ask someone who might know a little bit about the subject to give you […]

  • May 13, 2012

You could have invented fractional cascading

Suppose that you have k sorted arrays, each of size n. You would like to search for single element in each of the k arrays (or its predecessor, if it doesn't exist). Obviously you can binary search each array individually, resulting in a runtime. But we might think we can do better that: after all, […]

  • March 5, 2012

Visualizing range trees

Range trees are a data structure which lets you efficiently query a set of points and figure out what points are in some bounding box. They do so by maintaining nested trees: the first level is sorted on the x-coordinate, the second level on the y-coordinate, and so forth. Unfortunately, due to their fractal nature, […]

  • February 26, 2012

Anatomy of “You could have invented…”

The You could have invented... article follows a particular scheme: Introduce an easy to understand problem, Attempt to solve the problem, but get stuck doing it the "obvious" way, Introduce an easy to understand insight, Methodically work out the rest of the details, arriving at the final result. Why does framing the problem this way […]

  • February 23, 2012

How to build DRM you can trust

Abstract. Proof-carrying code can be used to implement a digital-rights management scheme, in the form of a proof-verifying CPU. We describe how this scheme would work and argue that DRM implemented this way is both desirable and superior to trusted (“treacherous”) computing schemes. This scheme permits users to retain control over their own machines, while […]

  • February 15, 2012


Last night, I returned from my very first POPL, very exhausted, and very satisfied. It was great putting faces to names, chatting with potential PhD supervisors (both from the US and in the UK), and reveling in the atmosphere. Highlights from my files: Tony Hoare, on being awarded the ACM SIGPLAN Programming Languages Achievement Award, […]

  • January 28, 2012

Bugs and Battleships

Do you remember your first computer program? When you had finished writing it, what was the first thing you did? You did the simplest possible test: you ran it. As programs increase in size, so do the amount of possible tests. It’s worth considering which tests we actually end up running: imagine the children’s game […]

  • December 19, 2011