Nice, I was always turned off by the YC explanations I found, but this did the trick.

But the questions that's really not answered is: Is there anything useful for a programmer in pure CS, excluding AI? Does the ability to follow the gory papers at lambda-the-ultimate make you a better programmer (even if it is only for some obscure application)? Should I really spend a day getting intimate with the Curry-Howard isomorphism?