Введение в Coq

09.04.2025

Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).

Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?

Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.

И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах рассказывает об языке программирования Coq, формальных методах и зависимых типах.

Если вы хотите участвовать: ✔️ установите платформу ROCQ на свой компьютер ✔️ либо воспользуйтесь онлайн-IDE

Материалы к воркшопам можно найти в репозитории.

Записи воркшопов вы найдёте на YouTube.

В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.