Теория языков программирования
Theorem Provers и формальная верификация
seL4 - единственное ядро ОС в мире с математическим доказательством отсутствия buffer overflows, use-after-free и deadlocks. Оно используется в Darpa drone systems и L4Re hypervisor. Это не будущее - это уже реальность.
- **CompCert**: верифицированный C компилятор используется в авиации (DO-178C). Airbus A380 бортовые системы написаны с его использованием
- **CertiKOS**: верифицированный гиперквизор OS kernel для concurrent x86. Используется как основа для формально верифицированных виртуальных машин
- **Lean 4 + Mathlib**: математическое сообщество формализует теоремы. Fields Medalist Peter Scholze сотрудничает с Lean для верификации сложнейших математических результатов
Curry-Howard соответствие
Curry-Howard соответствие (Propositions as Types): типы соответствуют логическим утверждениям, программы - доказательствам. Функция типа A -> B - это доказательство 'из A следует B'. Конструирование термa нужного типа = построение доказательства.
По Curry-Howard, что соответствует функции A -> B?
Тактики доказательств
Тактики - команды для интерактивного построения доказательства. В Coq/Lean программист описывает цель (goal) и применяет тактики которые трансформируют цель в подцели. Процесс похож на интерактивное программирование.
Чем тактики отличаются от обычного программирования?
Proof Assistants
Proof assistant (interactive theorem prover) - система для построения и проверки формальных доказательств. Coq, Lean 4, Isabelle/HOL, Agda - основные системы. Каждое доказательство проверяется kernel - маленьким, верифицируемым ядром.
Что гарантирует proof kernel в Coq/Lean?
Формальная верификация программ
Формальная верификация - доказательство корректности программ относительно спецификации. CompCert - верифицированный C компилятор (Coq). seL4 - верифицированный микроядро ОС. CryptoProof - верифицированные криптографические протоколы.
Formal verification слишком дорога для производственного кода - только для академии
seL4 используется в критических системах (военная авиация, автономные автомобили). Для 10% наиболее критического кода верификация окупается
Стоимость бага в safety-critical системе может быть катастрофической. Аэрокосмос, медицина, криптография - области где верификация дешевле отзыва продукта или человеческих жертв
Чем формальная верификация отличается от extensive testing?
Итоги
- **Curry-Howard**: типы = утверждения, программы = доказательства. A -> B = импликация. A × B = конъюнкция
- **Тактики**: интерактивное построение доказательства через цель -> подцели. Induction, rewrite, reflexivity
- **Proof assistants**: Coq/Lean/Isabelle. Маленький верифицируемый kernel - финальный судья корректности
- **Формальная верификация**: CompCert (C компилятор), seL4 (ОС ядро). Для safety-critical систем дешевле катастрофы
Связанные темы
Theorem proving связан с типами и верификацией:
- Model checking — Model checking - автоматический для ограниченных систем. Theorem proving - для произвольных программ но требует усилий
- Системы типов — Зависимые типы (Agda, Idris) объединяют типы и доказательства через Curry-Howard
Вопросы для размышления
- Curry-Howard означает что программирование и доказательство теорем - одно и то же. Как это меняет взгляд на систему типов в Rust или Haskell?
- CompCert верифицирован, но его генерация кода менее оптимальна чем gcc -O2. В авиации используется он, в браузере - gcc. Как выбирать когда верификация важнее производительности?
- seL4 верифицирован на конкретной платформе (ARMv7). При портировании на ARMv8 нужно переверифицировать. Насколько это практично для реальных систем?