FProg (Октябрь 2016)

Idris: неужели дождались? — Игнат Толчанов

Несмотря на то, что зависимые типы — концепция далеко не новая, большей части разработчиков они неизвестны, большей части остальных же они кажутся драматически далёкими от их реальных проблем. Не в последнюю очередь эта ситуация сложилась благодаря инструментам и языкам программирования, ориентированным в большей степени на исследовательскую работу, нежели на коммерческую разработку. Но несколько лет назад появился Idris: язык с поддержкой зависимых типов, задуманный как язык программирования общего назначения.

В ходе доклада будет проведён краткий обзор возможностей языка с использованием примеров, максимально приближенных к реальностям сурового энтерпрайза.

Доказательство свойств программ — введение в Coq — Андрей Ляшин

1. Тестирование vs Доказательство.

2. Какие программы можно доказать (индуктивные типы, конструктивные построения, интуиционисткая логика, и структурно редуцирующая рекурсия)?

3. Почему это возможно (изоморфизм Карри-Ховарда и все такое)?

4. Что доказать нельзя (Тьюринг полнота и обязательна ли она)?

5. Как сформулировать доказываемую спецификацию?

6. Это упрощает или усложняет жизнь?

7. Что делать, если понравилось?

В унисон с поющим драконом: ответы на ЧаВо (Idris) — Антон Трунов

1. От пустого типа к семействам типов: неформальное введение.

2. А нам не всё равно: разбираемся с `=`, `==` и `decEq`.

3. Используй тотальные функции, Люк: примеры.

4. Боремся за тотальность строго и положительно: strict positivity.

5. Доверяй, но проверяй: верифицированные функторы, аппликативные функторы и монады.

6. Как перестать беспокоиться о хвостовой рекурсии и начать жить: пишем `map`.

Афтепати
В Puberty 

Программа встречи может быть уточнена