Логика и программирование: от алгоритма до верификации

Программа как логическое доказательство

Каррая-Говарда соответствие (Curry-Howard correspondence): программы и доказательства — одно и то же. Тип в программировании соответствует высказыванию в логике; программа, реализующая этот тип, — доказательству этого высказывания. Это не метафора — это строгая математическая связь.

Следствие: языки программирования с богатыми системами типов (Haskell, Coq, Agda) позволяют кодировать логические ограничения в сам код — так, что некорректная программа просто не скомпилируется. «Тип системы — спецификация; компилятор — верификатор».

Формальная верификация программ: математическое доказательство того, что программа соответствует спецификации. Используется в критически важных системах: ядерные реакторы, авиация, медицинские устройства. В 2022 году компилятор CompCert (формально верифицированный компилятор C) первым получил формальное доказательство корректности — на 6 человеко-лет работы.

Алгоритмическая сложность и практика

P vs. NP — главный открытый вопрос информатики. Практические следствия. Коммивояжёр (TSP): для n городов найти кратчайший маршрут. NP-полная задача — нет известного полиномиального алгоритма. Для 1000 городов перебор требует больше операций, чем атомов во Вселенной. Применяются эвристики: генетические алгоритмы, имитация отжига.

Алгоритмы быстрой сортировки — практически O(n log n), теоретически O(n²) в худшем случае. Алгоритм Дейкстры — кратчайший путь — O(V²) или O(E log V). Это знания, влияющие на производительность любой IT-системы.

«Нет бесплатного обеда» (No Free Lunch theorem): нет алгоритма оптимизации, превосходящего все другие на всех задачах. Алгоритм, лучший для одного класса задач, хуже для других. Это математически доказанная причина, почему «универсального» ИИ не может быть.

Вопрос для размышления: Алгоритмическое мышление — разбиение задачи на детерминированные шаги. Какие задачи в вашей работе поддаются алгоритмизации, а какие требуют суждения, которое нельзя алгоритмизировать?