Описание

О чем курс

Курс рассказывает о том как писать правильные программы и как строго доказывать, что они правильные. О том, что значит правильные программы мы тоже поговорим. Рассказ построен вокруг системы интерактивного доказательства теорем Coq, теории типов, лежащей в ее основе, и применения Coq к задачам программирования.

Если же вас когда-нибудь мучали сомнения в правильности вашего (неформального) доказательства какой-нибудь леммы или теоремы, то в этом курсе мы научимся больше не сомневаться (почти), а использовать компьютер для проверки доказательств. Мы изучим несколько языков (в том числе мета-языков) и вдоволь повеселимся, доказывая всякую всячину про функциональные алгоритмы: посортируем списки и повертим деревья -- очень полезный навык для собеседований ;)

Пререквизиты к курсу

• Базовое функциональное программирование

• Желательно: элементы математической логики

Родственные курсы

• Семантика языков программирования
• Мой курс по формальной верификации в МФТИ, осень 2019

Что почитать

• Constructive Logic от Frank Pfenning
• Programs and Proofs от Ильи Сергея
• Mathematical Components от Assia Mahboubi и Enrico Tassi
• SSReflect Cheatsheet

Что нужно иметь с собой на занятиях

Вам будет нужен компьютер с установленным Coq и средой для редактирования: CoqIDE или VsCoq (плагин для VSCode) или Proof General (мод для Emacs).

Где прочитать про установку

Как установить Coq можно найти в wiki: https://github.com/coq/coq/wiki#coq-installation. Если установка по wiki не получается, то посмотрите еще вот это описание, содержащее рецепты для Ubuntu и macOS. Если у вас Windows, то лучшим вариантом будет использование инсталлятора со страницы релизов -- инсталлятор содержит наиболее популярные библиотеки и плагины для Coq, в том числе Mathcomp.

Если вам нужна помощь с установкой, то, пожалуйста, обратитесь ко мне до первого занятия (Телеграм: AntonTrunov) -- установка может занять достаточно много времени (иногда требуется компиляция из исходников).

Версии программ/библиотек, которые нам понадобятся

• Coq версии 8.11 (текущий патч-релиз на момент написания -- 8.11.0)
• библиотека Mathcomp версии 1.10
• среда для редактирования может быть любой относительно недавней версии

Как понять, что все установилось правильно

В псевдо-IDE по вашему выбору введите

From mathcomp Require Import ssreflect.

и выполните команду сделать шаг или проверить весь файл. В результате может появиться много предупреждений, но не должно быть ошибки вида

Error: Unable to locate library
ssreflect with prefix mathcomp. (While searching for a .vos file.)

Запасные варианты

• JsCoq Interactive Online System -- можно запустить Coq в браузере
• ссылка на виртуальную машину с Ubuntu (логин/пароль: coq/coq)

Что студенты будут уметь после окончания курса

После успешного прохождения курса слушатель:

• Владеет основами конструктивистской логики и теории типов, умеет транслировать утверждения естественного языка на язык логики высшего порядка

• Имеет практический навык компьютерных доказательств с помощью Coq, в том числе знает основные эвристические приемы доказательств по индукции

• Имеет представление об основных аксиомах, которые часто используют в проектах по формализации

• Имеет базовый навык специфицирования и доказательства корректности функциональных алгоритмов

• Умеет играть на фортепиано (если раньше уже умел)

• Владеет языком доказательств SSReflect, ориентируется в библиотеке Mathcomp и понимает ее основные архитектурные решения и подходы

• Умеет программировать вывод типов при помощи канонических структур и понимает особенности работы одного из алгоритмов унификации в Coq

Критерии оценивания

Оценка за курс будет в равной степени состоять из результата выполнения практических заданий в течение курса, а также двух устных экзаменов в середине и в конце курса.