Октябрьская встреча сообщества функциональных программистов
Октябрьская встреча любителей и профессионалов функционального программирования в Санкт-Петербурге, посвящённая зависимым типам и автоматическому доказательству теорем.
Idris: неужели дождались? — Игнат Толчанов
Несмотря на то, что зависимые типы — концепция далеко не новая, большей части разработчиков они неизвестны, большей части остальных же они кажутся драматически далёкими от их реальных проблем. Не в последнюю очередь эта ситуация сложилась благодаря инструментам и языкам программирования, ориентированным в большей степени на исследовательскую работу, нежели на коммерческую разработку. Но несколько лет назад появился Idris: язык с поддержкой зависимых типов, задуманный как язык программирования общего назначения.
В ходе доклада будет проведён краткий обзор возможностей языка с использованием примеров, максимально приближенных к реальностям сурового энтерпрайза.
Доказательство свойств программ — введение в Coq — Андрей Ляшин
- Тестирование vs Доказательство.
- Какие программы можно доказать (индуктивные типы, конструктивные построения, интуиционисткая логика, и структурно редуцирующая рекурсия)?
- Почему это возможно (изоморфизм Карри-Ховарда и все такое)?
- Что доказать нельзя (Тьюринг полнота и обязательна ли она)?
- Как сформулировать доказываемую спецификацию?
- Это упрощает или усложняет жизнь?
- Что делать, если понравилось?
Афтепати В Puberty
 |