На ICFP небезызвестный Бенджамин Пирс сделал очень интересный, на мой взгляд, доклад Lambda, the Ultimate TA: Using a Proof Assistant to Teach Programming Language Foundations, в котором он рассказывает о преподавании основ языков программирования с помощью доказывателя теорем (proof assistant), в данном случае это был coq. Материалы курса доступны на личной странице Бенджамина.
Интересно, в России (ну или где-то ещё на постсоветском пространстве) преподают Computer Science на подобном уровне?
Re[7]: Использование доказывателей теорем для обучения основ
Здравствуйте, Курилка, Вы писали:
D>>Ага, 05.13.17 Теоретические основы информатики. В физмат науках с натяжкой подойдет разве что: 01.01.09 Дискретная математика и математическая кибернетика.
К>А где они такие у нас есть?
Судя по данным отсюда есть в СПбГУ. Совет по защите на матмехе, думаю и аспирантура там же.
Re[4]: Использование доказывателей теорем для обучения основ
Здравствуйте, deniok, Вы писали:
D>Да, я посмотрел; и еще раньше читал его описание этого курса (где-то была статья несколько месяцев назад). Это не базовый курс "для масс" (даже с CS факультета приличного штатовского университета). Если его и делать базовым, то для специализации Theoretical Computer Science. У нас, кстати, в России есть подобная специализация, не знаешь?
Смотрим специальности аспирантуры 05.13.хх — там есть теоретическая информатика. А еще в физмат-науках что-то похожее есть.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Re: Использование доказывателей теорем для обучения основ ЯП
Здравствуйте, Курилка, Вы писали:
К>Интересно, в России (ну или где-то ещё на постсоветском пространстве) преподают Computer Science на подобном уровне?
Это же уже уровень, когда довольно крупный ученый (и отличный преподаватель по совместительству) читает авторский курс. У нас в Петербурге нечто подобное есть в Computer Science клубе при ПОМИ РАН.
Re[2]: Использование доказывателей теорем для обучения основ
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, Курилка, Вы писали:
К>>Интересно, в России (ну или где-то ещё на постсоветском пространстве) преподают Computer Science на подобном уровне?
D>Это же уже уровень, когда довольно крупный ученый (и отличный преподаватель по совместительству) читает авторский курс. У нас в Петербурге нечто подобное есть в Computer Science клубе при ПОМИ РАН.
Ну если ты посмотришь само видео, то Бенджамин как раз другие цели ставит — сделать курс не для гиков, а для более широкой аудитории. Поэтому он и выложил материалы на веб, чтоб другие могли использовать для проведения курсов.
Хотя курса "для масс" не получилось, по его словам
Re[3]: Использование доказывателей теорем для обучения основ
Здравствуйте, Курилка, Вы писали:
К>Ну если ты посмотришь само видео, то Бенджамин как раз другие цели ставит — сделать курс не для гиков, а для более широкой аудитории. Поэтому он и выложил материалы на веб, чтоб другие могли использовать для проведения курсов. К>Хотя курса "для масс" не получилось, по его словам
Да, я посмотрел; и еще раньше читал его описание этого курса (где-то была статья несколько месяцев назад). Это не базовый курс "для масс" (даже с CS факультета приличного штатовского университета). Если его и делать базовым, то для специализации Theoretical Computer Science. У нас, кстати, в России есть подобная специализация, не знаешь?
Re[4]: Использование доказывателей теорем для обучения основ
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, Курилка, Вы писали:
К>>Ну если ты посмотришь само видео, то Бенджамин как раз другие цели ставит — сделать курс не для гиков, а для более широкой аудитории. Поэтому он и выложил материалы на веб, чтоб другие могли использовать для проведения курсов. К>>Хотя курса "для масс" не получилось, по его словам
D>Да, я посмотрел; и еще раньше читал его описание этого курса (где-то была статья несколько месяцев назад). Это не базовый курс "для масс" (даже с CS факультета приличного штатовского университета). Если его и делать базовым, то для специализации Theoretical Computer Science. У нас, кстати, в России есть подобная специализация, не знаешь?
Ну про "базовый" никто вроде не говорил
А про специализацию — мне из нашей провинции гораздо хуже видно, чем тебе с Питера.
Re[5]: Использование доказывателей теорем для обучения основ
Здравствуйте, LaptevVV, Вы писали:
LVV>Здравствуйте, deniok, Вы писали:
D>>Да, я посмотрел; и еще раньше читал его описание этого курса (где-то была статья несколько месяцев назад). Это не базовый курс "для масс" (даже с CS факультета приличного штатовского университета). Если его и делать базовым, то для специализации Theoretical Computer Science. У нас, кстати, в России есть подобная специализация, не знаешь? LVV>Смотрим специальности аспирантуры 05.13.хх — там есть теоретическая информатика. А еще в физмат-науках что-то похожее есть.
Ага, 05.13.17 Теоретические основы информатики. В физмат науках с натяжкой подойдет разве что: 01.01.09 Дискретная математика и математическая кибернетика.
Re[6]: Использование доказывателей теорем для обучения основ
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, LaptevVV, Вы писали:
LVV>>Смотрим специальности аспирантуры 05.13.хх — там есть теоретическая информатика. А еще в физмат-науках что-то похожее есть.
D>Ага, 05.13.17 Теоретические основы информатики. В физмат науках с натяжкой подойдет разве что: 01.01.09 Дискретная математика и математическая кибернетика.
А где они такие у нас есть?
Re[6]: Использование доказывателей теорем для обучения основ
Здравствуйте, deniok, Вы писали:
LVV>>Смотрим специальности аспирантуры 05.13.хх — там есть теоретическая информатика. А еще в физмат-науках что-то похожее есть.
D>Ага, 05.13.17 Теоретические основы информатики. В физмат науках с натяжкой подойдет разве что: 01.01.09 Дискретная математика и математическая кибернетика.
Еще можно по специальностям 05.13.01 и 05.13.18 более математические диссеры делать.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
