Math is just a corner of computer science

[thedeemon]

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

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

Comments

[iigoncharenko.livejournal.com]

А я все книжки и лекции помечаю в файле. Под старость - опубликую в журнале (если склероз меня не пересилит).
На вскидку - начал читать книжки по Scala, но CT и монады там вообще не объяснялись, а поминались вскользь.
Пришлось читать хаскель (PIH, LYAH, RWH).
Непомню в какой момент, но жутко понравились "The Little ..." книжки Фридмена. Позже в одной из коммандировок в Индианаполись познакомился с одним из его студентов - узнал, что сам Фридмэн вообще недолюбливал книжки, предпочитая им рисовать картинки и объяснять наглядно.
А когда стал смотреть статьи, то понял что без TAPL и CT (выбрал для себя Awodey-я) толку не будет.
Об этом кстати и сам Харпер в лекциях говорил (CS держится на 3-х китах: Logic, Typed-LC, CT).

[thedeemon.livejournal.com]

> "The Little ..." книжки Фридмена

А что это? Я как-то пропустил.

[iigoncharenko.livejournal.com]

Это - альтернанива SICP:
- The Little Schemer
- The Seasoned Schemer
- The Reasoned Schemer (купил, но ещё не читал)
- The Little Javer
- The Little MLer (даже не покупал ещё)

[thedeemon.livejournal.com]

А, спасибо! The Little Schemer встречал название, про остальных даже не слышал.

[lelf.livejournal.com]

Ну её стоит открыть посмотреть ;-) даже если не читать

[valentin budaev (from livejournal.com)]

> (CS держится на 3-х китах: Logic, Typed-LC, CT).

Давайте говорить более корректно. В CS есть такое мааахонькое ответвление - programming languages. И в этом мааахоньком ответвлении есть мааахонькое подответвление - системы типов. И только оно держится на указанных трех китах.

Не стоит выдавать этот вот крохотный и практически незаметный кусочек CS за весь CS.

[iigoncharenko.livejournal.com]

Пардно, я не совсем точно процитировал. Он говорил о том, что все дейстительно стоящие вещи, а не фуфел типа OOP... держатся на этих китах.
Кстати, а как Вы знакомились с FP (если знакомились, конечно) ?

[valentin budaev (from livejournal.com)]

> Он говорил о том, что все дейстительно стоящие вещи, а не фуфел типа OOP

OOP это тоже programming languages. Основная часть CS связана с теорией алгоритмов и соответствующей математикой.

> Кстати, а как Вы знакомились с FP

Как-то прямо намеренно с FP я не знакомился, не стояло такой задачи, но если хронологически относящееся к ФП, то
SICP, TAPL, RWH, разные papers на протяжении этого.

[iigoncharenko.livejournal.com]

Спасибо.

Про OOP-PL - совершенно верно. Когда-нибудь PL-и будут очень сильно-типизированы (на грани DependentTypes и т.д) и тогда все товарищи типа Харпера вдруг переключат внимание на дизайн алгоритмов и структур данных.