ezyang’s blog

the arc of software bends towards understanding

November, 2010

My first proof in Isabelle

One of the distinctive differences between academic institutions in the United States and in Great Britain is the supplementary learning outside of lectures. We have recitations in the US, which are something like extra lectures, while in the UK they have tutorials, or supervisions as they are called in Cambridge parlance. As always, they are […]

  • November 29, 2010

Reflexivity. Qed.

In which Mendeley, Software Foundations and Coq are discussed. I was grousing on #haskell-blah one day about how annoying it was to organize all of the papers that I have downloaded (and, of course, not read yet.) When you download a paper off the Internet, it will be named all sorts of tremendously unhelpful things […]

  • November 26, 2010

Integer sequences every computer scientist should know?

The On-Line Encyclopedia of Integer Sequences is quite a nifty website. Suppose that you’re solving a problem, and you come up with the following sequence of integers: 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2... and you wonder to yourself: “huh, what’s that sequence?” Well, just type it in and the […]

  • November 24, 2010

Is multiply-carry strongly universal?

I’ve been wanting to implement a count-min sketch for some time now; it’s a little less widely known than the bloom filter, a closely related sketch data structure (that is, a probabilistic data structure that approximates answers to certain queries), but it seems like a pretty practical structure and has been used in some interesting […]

  • November 22, 2010

Cambridge potpourri

In which Edward tells some stories about Cambridge and posts lots of pictures. Apparently, Alyssa B. Hacker (sic) went on the Cambridge-MIT exchange. This is perhaps a phenomenon of having been around MIT for too long, a campus which has a reputation for not being too picturesque (I can probably count the actually pretty spots […]

  • November 19, 2010

Haskell.org committee

Ever try to go to haskell.org and notice that it was down? Well, now you have someone to complain to: the haskell.org committee has formed and apparently I’m on it. 8-) One of the first things we’ll be doing is moving haskell.org from a server being hosted at Yale (the hosting has been good, but […]

  • November 17, 2010

It’s just a longjmp to the left

And then a signal to the ri-i-i-ight. One notable wart with readline is that if you ^C during the prompt, nothing happens, and if you do a second ^C (and weren’t buggering around with the signal handlers) your entire program unceremoniously terminates. That’s not very nice! Fortunately, readline appears to be one of the rare […]

  • November 15, 2010

mod_fcgid 2.3 is broken (fixed in 2.3.6)

This is a post to get some Google juice for a problem that basically prevented Scripts from being able to cut over from Fedora 11 to Fedora 13. The cluster of new machines kept falling over from load, and we kept scratching our heads, wondering, “Why?” Turns out, the following commit broke mod_fcgid in a […]

  • November 10, 2010

Medieval medicine and computers

This is a bit of a provocative post, and its impressions (I dare not promote them to the level of conclusions) should be taken with the amount of salt found in a McDonald’s Happy Meal. Essentially, I was doing some reading about medieval medicine and was struck by some of the similarities between it and […]

  • November 8, 2010