ср, 09 апрель 2025, 19:00 (GMT+03:00)
	Бесплатно
	Есть трансляция
	Московский клуб программистов

Теги: coq зависимые типы верификация программ

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

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

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

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

Первый воркшоп будет посвящён основам программирования на языке Coq.

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

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

Ждём вас на первом воркшопе в среду 9 апреля в 19:00 на трансляции в YouTube или VK.

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

Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Добавить в календарь