Введение в Coq: формальные методы и зависимые типы, Часть IV

Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо). Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код? Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать. И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах. Четвёртый воркшоп посвятим спискам, деревьям и математической индукции. Если вы хотите участвовать: ✔️установите платформу ROCQ на свой компьютер:
✔️либо воспользуйтесь онлайн-IDE:
Материалы к воркшопам можно найти в этом репозитории:
В организации трансляций нам помогает наш партнёр SBTG.RU (
Трансляции в любых конфигурациях под ключ. Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting (
Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.