the arc of software bends towards understanding
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." […]
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 […]
“...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 […]
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 […]
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, […]
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, […]
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 […]
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 […]
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, […]
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 […]