О чем курс

Формальная верификация программ — это набор парадигм, техник и инструментов, гарантирующих с той или иной степенью надёжности корректность программ. Думаю многие согласятся, что есть области ИТ, в которых корректность заслуживает самого пристального внимания: прошивки бортовых компьютеров самолетов, автомобилей, кардиостимуляторов, софт атомных электростанций и др.

Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем Coq (https://coq.inria.fr), теория типов, лежащей в ее основе, метапрограммирование в Coq и применение Coq к верификации функциональных алгоритмов.

Лекции будут читаться через zoom. Ссылка для подключения будет опубликована в новостях курса (её получат те, кто запишется на курс).

Материалы к курсу

По мере прохождения курса материалы будут выкладываться в репозитории по адресу: https://github.com/anton-trunov/csclub-coq-course-spring-2021.

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

• Базовое функциональное программирование (анонимные функции, рекурсия, функции высшего порядка, алгебраические типы данных, паттерн-матчинг)
• Классическая (или интуиционистская) логика высказываний и логика предикатов.

Программа курса

1. Введение в курс, основы тотального функционального программирования в Coq, интерактивные запросы в Coq
2. Алгебраические типы данных, элементы соответствия Карри-Говарда, интуиционистская пропозициональная логика. Зависимые типы и зависимый паттерн-матчинг, пропозициональное равенство, инъективность и дизъюнктивность конструкторов.
3. Кванторы всеобщности и существования. Доказательства по индукции. Индукция и рекурсия.
4. Язык тактик SSReflect. Виды индукции: математическая, парная, сильная. Эвристики для доказательств по индукции. Списки. Структурная индукция для списков.
5. Разрешимые свойства, reflect-предикат, виды и подсказки видов, спецификации и зависимые типы, коэрции.
6. Анализ случаев для семейств типов. adhoc полиморфизм и канонические структуры. Архитектура типа с равенством (eqType). Канонические миксины. Фантомные типы. Клонирующие конструкторы. Унификация и η-расширение.
7. Подтипирование. Неразличимость доказательств. Конечные типы, ординалы, кортежи.
8. Prop и Type. Непредикативность Prop, предикативность Type. Большая элиминация и закон исключенного третьего. Тотальность и завершаемость программ. Плагины Function, Program, Equations. Правило строгой позитивности для индуктивных типов. Полиморфизм по уровням вселенных. Парадокс Рассела в Coq.
9. Спецификация и верификация функциональных алгоритмов. Индуктивные предикаты. Деревья Брауна: подходы к реализации. Экстракция.
10. Рандомизированное тестирование свойств (QuickChick). Мутационное тестирование доказательств. Автоматизация доказательств: встроенные тактики, интеграция SMT-решателей в Coq, использование технологий, построенных на машинном обучении.

Пожалуйста, обратите внимание, что программа курса примерная и перечень тем, а также глубина их рассмотрения может корректироваться по ходу курса.

Чат курса

Телеграм: https://t.me/joinchat/Ge1_yrqEFxEzYjAy. В чате можно попросить помощи с инсталляцией (см. ниже), что-то уточнить, обсудить домашние задания, указать на ошибки/опечатки и т.п.

Базовая литература

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

Полезные ссылки

• Шпаргалка по SSReflect

Программное обеспечение для семинаров/практических занятий

Вам будет нужен компьютер со следующим установленным программным обеспечением

• Coq версии 8.13 (текущий патч-релиз на момент написания -- 8.13.1)
• библиотека Mathcomp версии 1.12.0
• одна из интерактивных сред для редактирования доказательств: CoqIDE или VsCoq (плагин для VSCode -- рекомендуется для начинающих) или Proof General (мод для Emacs). Cреда для редактирования может быть любой относительно недавней версии.

Важно: без интерактивной среды взаимодействие с Coq сильно усложняется. Если вы очень не любите среды для редактирования, то можно использовать интерпретатор coqtop, входящий в комплект поставки Coq.

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

В настоящий момент рекомендуемый способ установить Coq на Linux и Windows -- это воспользоваться Coq Platform, помимо Coq включающей в себя большое количество предустановленных библиотек. Про этот способ установки можно прочитать в wiki: https://github.com/coq/coq/wiki#coq-installation.

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

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

В интерактивной среде по вашему выбору введите

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 в браузере. Чтобы запустить JsCoq с пустым файлом воспользуйтесь следующей ссылкой: https://coq-next.vercel.app/scratchpad.html. Внимание: версии Coq и Mathcomp могут отличаться от используемых в курсе.