Math is just a corner of computer science

Несколько цитат из лекций Роберта Харпера из CMU про то, что важно в языках программирования, чему нас зря учили в школе, почему интуиционистская логика круче классической, и почему вовсе не математика царица наук:

Надергал из прошлогодних лекций в Oregon Programming Languages Summer School. Харпер там рассказывал основы теории типов - от элементарщины через зависимые типы до индуктивных типов высших измерений и гомотопической теории типов (про последние, правда, совсем немного). Кроме него там много других замечательных лекций: Awodey про теоркат, Xavier Leroy про верификацию компиляторов, John Hughes про монады и др. Просто праздник какой-то. Ссылка года, вот она:
http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html