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

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

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