Functional Data Structures and Algorithms: a Proof Assistant Approach
Книга вводит структуры данных и алгоритмы для функциональных языков с акцентом на доказательства. Она охватывает функциональную корректность и анализ времени выполнения в едином подходе: индуктивные доказательства применяются как к самим программам, так и к их функциям времени. Подходит для изучения в функциональном стиле, с примерами и полными формальными проверками.
Все доказательства machine-checked в доказательном ассистенте Isabelle; PDF-версия содержит гиперссылки на соответствующие теории Isabelle для самостоятельной верификации. Книга открыта для эволюции — авторы приглашают к вкладу и совместной доработке. Доступны изображения обложки и содержания для скачивания полного PDF.
Комментарии (15)
- Обсуждение книги: доказывает корректность напрямую, runtime — через абстракцию реального кода; вопрос о языках для прямых runtime-доказательств.
- Спор о binary search: критика за игнор стоимости сортировки (линейный поиск лучше для одного запроса); защита — алгоритм только для отсортированных данных.
- Верификация imperative кода крайне сложна из-за edge-кейсов и реальности; пример verified imperative программы в Lean.
- Binary search применим без начальной сортировки, напр. для поиска точки вставки в отсортированную структуру.
Why don't you use dependent types? 🔥 Горячее
Автор объясняет, что Isabelle сознательно отказалась от объектов доказательств, которые являются неотъемлемой частью обычных теорий типов. Это сделано потому, что объекты доказательств не нужны и занимают много места. Вместо этого Isabelle использует архитектуру LCF, где проверка типов осуществляется в языке реализации, а не в логике, что гарантирует легитимность шагов доказательства. Robin Milner имел это фундаментальное понимание 50 лет назад.
Лоуренс Полсон рассказывает о своем опыте работы с AUTOMATH и Martin-Löf type theory. Первоначально Isabelle была реализацией Martin-Löf type theory, которая до сих пор включена в дистрибутив как Isabelle/CTT. Однако автор переключился на более общий подход, вдохновленный AUTOMATH - "большим рестораном, который обслуживает любую кухню". В итоге Isabelle/HOL стала доминирующей, хотя де Брёйн не одобрял растущую мощь теорий типов и презирал теорию множеств.
Комментарии (98)
- Обсуждение показало, что вопрос не в «плохих» зависимых типах, а в том, что они не нужны для большинства задач и не оправдывают свою сложность.
- Участники обсуждали, что отсутствие зависимых типов не мешает Isabelle/HOL доказать критически важные части математики, и что вместо этого важнее автоматизация и библиотеки.
- Сообщество отметило, что даже в языках без зависимых типов можно выразить «матрица 10×5 из float32», если размеры известны на этапе компиляции, и что это покрывает большинство практических случаев.
- Несколько участников поделились личным опытом, что попытка использовать зависимые типы в продакшене привела к тому, что команды отказались их использовать из-за кривой кривой обучения и отсутствия инструментальной поддержки.
- В итоге автор статьи подытожил, что выбор между зависимыми типами и другими системами типов часто сводится к личным предпочтениям и доступным инструментам, а не к объективным преимуществам.