## Friday, December 14, 2007

### New York in Grainy Pictures

My three months in New York are over, so no more xiaolongbao at Yeah Shanghai, long rides on the New Jersey Transit trains, seminars on additive combinatorics, and hot pot at Minni's Shabu Shabu for me.

The other night, the traffic information board on 110th and Amsterdam was saying "CCCOOORRR... FFFFFF... AAAUUUU" which is how I too felt about the weather.

This is probably meant to lure in Italian tourists

The Apple store on 5th avenue open at 2:40am (and through the night), because it's never too late (or too early) to buy an iPhone

In the Canal stop of the N-Q-R-W. There were no signs in other languages.

I agree, it's good.

## Tuesday, December 11, 2007

### Happy Belated Birthday!

I just discovered, via CNN, that the Commodore 64 turned 25 last summer.

People that have met me later in life may be surprised to learn that I spent long hours programming for fun. Not that I need to be defensive or anything, and I certainly did not know so then, but, at the time, programming, even in the very basic Basic that came with the computer, was the closest thing I could do to math. Certainly, it was much closer than the "math" I was getting in school, which consisted in learning how to run certain numerical and algebraic algorithms by hand. Indeed I don't think I encountered anything closer to math than programming until the first year of college, when the whole notion of axioms, theorems, proofs, and playing a game with meaningless symbols'' was unloaded on me in a course innocuously termed Geometry.'' (Nominally a course on linear algebra, the course was a parody of Bourbakism as a teaching style. In the first class the professor came in and said, a vector space is a set with two operations that satisfy the following nine axioms. Now I should like to prove the following proposition... I am not joking when I say that the fact that the elements of a $k$-dimensional vector space are $k$-tuples of numbers came as a revelation near the very end of the course.)
The fact that the type'' of a program is similar to a statement and the
implementation of a program is similar to a proof should be familiar to anybody who has written both. In both cases, one needs to break down an idea into basic steps, be very precise about how each step is realized, if a sequence of steps is repeated twice in a similar way one should abstract the similarity, write the abstracted version separately, and then use the abstracted version twice, and so on. The Curry-Howard isomorphism establishes this connection in a formal way, between a certain way of writing proof (say, Gentzen proof system with no cut in intuitionistic logic) and a certain way of writing programs (say, typed $\lambda$-calculus). I know because I once took a course based on the totally awesome book Proofs and Types by Girard, which is out of print but available for free on the web.