Existential Pontification and Generalized Abstract Digressions

## 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

## POPL

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

## Interactive Demo of Zero-Knowledge Proofs

For the final project in our theoretical computer science and philosophy class taught by Scott Aaronson, Karen Sittig and I decided to create an interactive demonstration of zero-knowledge proofs. (Sorry, the picture below is not clickable.) For the actually interactive demonstration, click here: http://web.mit.edu/~ezyang/Public/graph/svg.html (you will need a recent version of Firefox or Chrome, since […]

• December 17, 2011