tgoop.com/progmsk_channel/306
Last Update:
Введение в Coq: формальные методы и зависимые типы, Часть VII
⏰ Tue, 01 July 2025, 19:00 (+0300)
📺 Stream
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Седьмой воркшоп посвятим транспиляции Coq-программ на другие языки программирования, в частности, в OCaml. В терминах Coq этот процесс называется извлечением.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE: https://jscoq.github.io/scratchpad.html
Материалы к воркшопам можно найти в этом репозитории.
Ждём вас на седьмом воркшопе во вторник 1 июля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
Subscribe to new events in the bot @NetworklyBot
BY Prog.Msk • Channel
Share with your friend now:
tgoop.com/progmsk_channel/306