1 июля 2025 года в 19:00 (мск) состоится воркшоп «Введение в Coq: формальные методы и зависимые типы, Часть VII».
Каждый программист знает, что тесты не спасают от ошибок. Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Седьмой воркшоп посвятим транспиляции Coq-программ на другие языки программирования, в частности, в OCaml. В терминах Coq этот процесс называется извлечением.
Онлайн,Введение в Coq: формальные методы и зависимые типы, Часть VII
Дата проведения: 01.07.2025. Начало в 19:00
Место проведения: Онлайн
- Анонс
- Программа
- Участники
- Спикеры
1 июля 2025 года в 19:00 (мск) состоится воркшоп «Введение в Coq: формальные методы и зависимые типы, Часть VII».
Каждый программист знает, что тесты не спасают от ошибок. Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Седьмой воркшоп посвятим транспиляции Coq-программ на другие языки программирования, в частности, в OCaml. В терминах Coq этот процесс называется извлечением.
