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

[chaource.livejournal.com]

Лѣтняя школа выглядитъ очень заманчиво, но... лекцiи Харпера предлагается слушать только послѣ освоенiя Мартина-Лефа и четырехъ другихъ книгъ продвинутаго содержанiя?? Другiе лекторы не выставляютъ такого списка требованiй...

[thedeemon.livejournal.com]

Там вроде как одна указана как пререквизит, а остальные как дополнительное чтение. Я ничего из того списка не читал, признаюсь, но лекции его оказались очень понятными.

[chaource.livejournal.com]

Качаю всѣ лекцiи, спасибо за ссылку! Только вотъ размѣры MP4 великоваты, надо будетъ сократить.

[dmitri-pavlov.livejournal.com]

Поток идей, всё же, идёт в другую сторону: от математики к информатике (= theoretical computer science).
В частности, гомотопическая теория типов и унивалентность придуманы Воеводским, который математик,
и придуманы они как улучшенные основания для математики.
Категории тоже были придуманы в математики, Эйленбергом и МакЛэйном, для алгебраической топологии.
А равно и монады и множество других вещей, которые сейчас используют в информатике.

А в обратную сторону потока идей особо не наблюдается.

[thedeemon.livejournal.com]

Про поток идей не спорю, но он все же о другом говорит. Что, с определенной точки зрения, вся конструктивная математика - это вычисления, и вся она - объект его любимой теории типов. Не зря Воеводский сотоварищи свои основания математики сразу в Coq фигачат. Теоремы - типы, доказательства - программы, математика - программирование.

[deni-ok.livejournal.com]

Арнольд приписывал Манину определение математики, как раздела лингвистики: "это наука о формальных преобразованиях одних наборов символов некоторого конечного алфавита в другие при помощи конечного числа специальных грамматических правил".

[dmitri-pavlov.livejournal.com]

Это всё равно, что утверждать,
что математика — раздел лингвистики,
ибо математические тексты пишутся
на естественном языке,
а естественные языки являются
предметом изучения лингвистики.
Coq, равно как и TeX, например, — всего
лишь вспомогательный инструмент.

[valentin budaev (from livejournal.com)]

Но это все имеет смысл только за тем, чтобы проверить уже существующее доказательство формальными методами, нового ничего так не получишь. По-этому для математиков оно совершенно не нужно, все вполне довольны сложившимся положением вещей (когда вопрос правильности доказательства сводится к консенсусу). Более того, есть определенные аргументы как раз против формальных методов проверки в пользу консенсуса.

[gabriel-irk.livejournal.com]

По-другому и быть не может! :)
Поскольку математика является разделом CS, все идеи, появляющиеся в ней, также являются идеями и в CS. А вот идеи CS, появляющиеся за пределами математики, не могут в неё просочиться, поскольку математикой не являются. :-D

[ext-1764477.livejournal.com (from livejournal.com)]

http://www.cs.uoregon.edu/research/summerschool/summer13/blog.html
"you will need to prove is that you are not a risk to emigrate to the United States"
Три пересадки из Москвы + беготня в посольство + accomodation + cash = 170 в рыло. Ну их.

[juan-gandhi.livejournal.com]

Огромное спасибо. Оценил.

Что, наступают наши времена, не прошло и 30 лет...

[maxim.livejournal.com]

Сильная страница, на нее можно просто смотреть и уже знание получаешь :-)

[iigoncharenko.livejournal.com]

Я пока ещё не всего Харпера досмотрел, но уже врезались в память идеи о диком искажении понятия переменной (variable) в современных языках программирования и идеи предикатов (predicates). Признаться по правде, именно за это и люблю лекции (в противоположность книгам). Лектор обычно смелее автора и порой такое интересное рассказывает, что диву даёшься.
Правда, не уверен пока, что мне захочется смотреть лекции Awodey-я после чтения его 300-страничной книги (обычные лекции Pierce-а после TAPL тоже скучноваты).

И вот ещё что интересно (вопрос ко всем) - а как (в какой последовательности и по каким источникам) кто учился FP и соотв. мат. части ???

[thedeemon.livejournal.com]

>именно за это и люблю лекции (в противоположность книгам). Лектор обычно смелее автора и порой такое интересное рассказывает, что диву даёшься.

+1! Тут как раз такой случай.
Awodey лекции я скачал, но пока не смотрел еще.

Кто как учился - вряд ли вспомнит. Часто это огромное количество обрывков книг, статей и блог-постов. Для меня fp началось с сайта-книжки Developing applications with Objective Caml. Из книг особенно запомнилась Type Theory & Functional Programming by Simon Thompson, вот только бросил я ее рано, надо бы дочитать. :) Из блогов sigfpe особенно хорош.

[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 и т.д) и тогда все товарищи типа Харпера вдруг переключат внимание на дизайн алгоритмов и структур данных.

[iigoncharenko.livejournal.com]

Ещё вот что интересно.
Когда впервые выложили видео лекций в 2012-м году поздним летом (я как рас был в коммандировке в Индианаполисе) - не было лекций Хьюза про монады.
Я долго потом проверял несколько раз с промежутками - их всё небыло.
А вчера посмотрел - они лежат :)
Вот я типа и дождался...