Основы формальной верификации в системе Coq

Введение в Coq: функциональное программирование на языке Gallina и базовые типы

Добро пожаловать в курс «Основы формальной верификации в системе Coq». Это первая статья, в которой мы заложим фундамент для всего дальнейшего обучения. Мы привыкли, что программы пишутся, тестируются и отправляются в продакшн. Но что, если цена ошибки слишком высока? В авиации, медицине, криптографии или финансовых системах обычного тестирования недостаточно. Здесь на сцену выходит формальная верификация — математическое доказательство того, что программа работает в строгом соответствии со своей спецификацией.

Инструмент, который мы будем изучать — Coq. Это интерактивная система доказательства теорем, которая позволяет не только формулировать математические утверждения и доказывать их, но и писать исполняемые программы. В основе Coq лежит язык функционального программирования Gallina.

Архитектура системы Coq

Прежде чем писать код, важно понять, с чем мы имеем дело. Coq — это не просто компилятор, это среда, объединяющая три сущности:

Gallina — язык спецификаций и программирования. На нем мы пишем алгоритмы и формулируем теоремы.

The Vernacular — командный язык для управления окружением Coq (команды вроде Check, Compute, Print).

Ltac — язык тактик для построения доказательств (о нем мы поговорим в следующих статьях).

!Диаграмма, показывающая взаимосвязь между языком Gallina, тактиками Ltac и командным языком Vernacular в экосистеме Coq.

Сегодня мы сосредоточимся исключительно на Gallina. Если вы знакомы с Haskell, OCaml или F#, многое покажется вам знакомым. Если нет — не переживайте, мы начнем с основ.

Объявление типов и значений

В Coq, как и в любом типизированном языке, каждое выражение имеет тип. Чтобы проверить тип выражения, используется команда Check.

Здесь nat обозначает натуральные числа, а bool — логический тип. Обратите внимание: каждая команда в Coq должна заканчиваться точкой.

Чтобы дать имя значению, мы используем ключевое слово Definition:

Это создает глобальное определение answer с типом nat (натуральное число) и значением 42.

Пользовательские типы данных

Мощь Gallina заключается в возможности создавать собственные типы. Самый базовый способ — это индуктивные типы (Inductive types). Давайте определим тип, представляющий дни недели.

Разберем этот код: * Inductive — ключевое слово для объявления нового типа. * day — имя нашего нового типа. * Type — это «тип типов» (сорт), указывающий, что day является типом данных. * monday, tuesday и так далее — это конструкторы типа day.

Теперь мы можем написать функцию, которая работает с этим типом. В функциональном программировании основным инструментом управления потоком является сопоставление с образцом (pattern matching).

Функции и сопоставление с образцом

Напишем функцию, которая определяет следующий рабочий день.

Здесь: * Definition объявляет функцию next_weekday. * (d : day) — аргумент функции d типа day. * : day после скобки указывает тип возвращаемого значения. * Конструкция match d with ... end проверяет значение d и возвращает соответствующий результат.

Мы можем проверить работу функции с помощью команды Compute:

Булев тип (Booleans)

В стандартной библиотеке Coq булев тип определен точно так же, как мы определили дни недели — через перечисление конструкторов:

Функции над булевыми значениями также определяются через сопоставление с образцом. Например, логическое отрицание:

И логическое «И» (конъюнкция):

Обратите внимание на лаконичность andb. Если b1 истинно, то результат зависит только от b2. Если b1 ложно, то результат всегда false, независимо от b2.

Натуральные числа: взгляд изнутри

Самый интересный момент для новичков в Coq — это представление чисел. В обычных языках программирования числа — это примитивы процессора (32 или 64 бита). В Coq натуральные числа (nat) определены математически, используя аксиоматику Пеано.

Определение выглядит так:

Это рекурсивное определение:

O (заглавная буква O) — это конструктор, представляющий ноль.

S — это конструктор, который принимает одно натуральное число и возвращает «следующее» за ним (Successor).

!Визуализация структуры натуральных чисел Пеано, где каждое число является оболочкой над предыдущим.

Таким образом: * представляется как O. * представляется как S O. * представляется как S (S O). * представляется как S (S (S O)).

Математически это записывается так:

Где — множество натуральных чисел, — начальный элемент, а — функция следования.

Рекурсивные функции

Поскольку числа определены рекурсивно, функции для работы с ними тоже должны быть рекурсивными. В Gallina для объявления рекурсивной функции используется ключевое слово Fixpoint вместо Definition.

Давайте определим функцию проверки на четность evenb:

Логика работы:

Если число — O (ноль), то оно четное (true).

Если число — S O (единица), то оно нечетное (false).

Если число имеет вид S (S n') (то есть ), то его четность совпадает с четностью . Мы рекурсивно вызываем evenb для .

Здесь — это переменная, которая связывается с «пред-предыдущим» числом.

Сложение чисел

Определение сложения также базируется на структуре чисел Пеано. Математически сложение можно определить так:

Где первая строка — это базовый случай (если первое слагаемое ноль), а вторая — рекурсивный шаг (мы выносим за скобки).

В коде Gallina это выглядит следующим образом:

Когда Coq вычисляет plus (S (S O)) (S O) (то есть ), он делает следующие шаги редукции:

plus (S (S O)) (S O)

S (plus (S O) (S O)) (сработала вторая ветка match)

S (S (plus O (S O))) (снова вторая ветка)

S (S (S O)) (сработала первая ветка, так как первый аргумент стал O)

Результат — S (S (S O)), что соответствует числу 3.

Строгая типизация и завершимость

Важно отметить одну особенность Gallina: все функции должны завершаться. В Coq нельзя написать бесконечный цикл while(true). Это необходимо для того, чтобы логика доказательств оставалась непротиворечивой.

Когда вы используете Fixpoint, Coq автоматически проверяет, что рекурсия «убывает». В примере с plus аргумент n уменьшается на каждом шаге (от S n' к n'), поэтому Coq разрешает такое определение. Если бы Coq не смог убедиться в завершении функции, он бы выдал ошибку компиляции.

Заключение

Мы познакомились с языком Gallina, научились определять простые типы данных, использовать сопоставление с образцом и писать рекурсивные функции для натуральных чисел. Это — алфавит, на котором мы будем писать не только программы, но и доказательства их корректности.

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

Основы логики и доказательств: пропозициональное исчисление и применение тактик

В предыдущей статье мы познакомились с языком Gallina, научились определять типы данных и писать простые функциональные программы. Однако главная сила Coq заключается не в вычислениях, а в доказательствах. Сегодня мы перейдем от написания кода к формальной логике.

Мы разберем, как формулировать логические утверждения, что такое «режим доказательства» и как использовать тактики для манипуляции логическими формулами. Наша цель — понять пропозициональное исчисление (логику высказываний) через призму системы Coq.

Утверждения как типы (Propositions as Types)

В Coq существует глубокая связь между программированием и доказательством, известная как изоморфизм Карри — Ховарда. Эта концепция может показаться сложной, но ее суть проста:

Утверждение (теорема) — это Тип.

Доказательство — это Программа (терм), имеющая этот тип.

Если в предыдущей лекции мы писали Definition n : nat := 5, то есть создавали число 5 типа nat, то теперь мы будем создавать «доказательство» для «утверждения».

В Coq для логических утверждений существует специальный сорт (тип типов), который называется Prop. Все математические теоремы, леммы и факты имеют тип Prop.

Структура доказательства

Чтобы начать доказательство, используются ключевые слова Theorem, Lemma, Fact или Example (для Coq они практически идентичны). Рассмотрим простейшее утверждение: «Если A влечет B, и мы знаем A, то верно B».

Здесь мы утверждаем, что для любых утверждений и (где и — логические высказывания типа Prop), если истинно и из следует , то истинно.

После ввода этой команды Coq переключает нас в интерактивный режим доказательства (Proof Mode). Вместо написания кода мы будем взаимодействовать с системой, отдавая ей команды — тактики.

!HB

Обратите внимание на синтаксис [HA | HB] с вертикальной чертой. Это означает, что мы создаем две ветки доказательства: в одной у нас есть гипотеза HA, в другой — HB.

!...

* Понимать отрицание как импликацию лжи.

Эти кирпичики позволят вам строить доказательства произвольной сложности. В следующей статье мы расширим наш арсенал, добавив кванторы существования и всеобщности, переходя к логике предикатов первого порядка.

Индуктивные типы данных, рекурсия и доказательство методом математической индукции

Добро пожаловать в третью часть курса «Основы формальной верификации в системе Coq». В предыдущих статьях мы изучили основы языка Gallina, определили натуральные числа и научились проводить простейшие логические доказательства с помощью тактик intros, exact и apply.

Однако, как только мы начинаем работать с рекурсивными структурами данных (такими как числа или списки) и пытаемся доказать их общие свойства, простых тактик становится недостаточно. Мы сталкиваемся с необходимостью использовать математическую индукцию.

В этой статье мы разберем, почему обычное упрощение кода не всегда работает, как устроена индукция в Coq и познакомимся с новой мощной тактикой rewrite.

Проблема: когда simpl бессилен

Вспомним определение сложения plus, которое мы рассматривали в первой лекции. Оно определено рекурсивно по первому аргументу:

Давайте попробуем доказать два похожих утверждения.

Утверждение 1:

Это доказательство проходит мгновенно. Почему? Потому что команда simpl (упрощение) смотрит на определение plus. Она видит, что первый аргумент — это O (ноль). Согласно первой ветке match в определении функции, plus O n вычисляется в n. Мы получаем равенство n = n, которое тривиально доказывается тактикой reflexivity.

Утверждение 2:

Казалось бы, от перестановки слагаемых сумма не меняется. Попробуем доказать это:

Здесь simpl не может ничего сделать. Функция plus ожидает, что первый аргумент будет либо O, либо S .... Но у нас первый аргумент — это переменная n. Coq не знает, чему равно n в данный момент, поэтому он не может выбрать ветку match и раскрыть определение.

Мы застряли. Чтобы доказать утверждение для любого n, нам нужен принцип индукции.

Принцип математической индукции

Для натуральных чисел принцип индукции звучит так: чтобы доказать, что свойство верно для всех натуральных чисел, нужно сделать два шага:

База индукции: Доказать, что верно.

Индуктивный шаг: Доказать, что если верно для некоторого , то тоже верно.

В формальной записи:

Где: * — доказываемое свойство (предикат). * — ноль. * — функция следования (следующее число за , то есть ). * — логическая импликация («следовательно»). * — квантор всеобщности («для всех»).

!Визуализация метода математической индукции через принцип домино: если первая костяшка упала, и каждая следующая падает вслед за предыдущей, то упадут все костяшки.

В Coq этот принцип реализуется тактикой induction.

Тактика induction

Вернемся к нашему застрявшему доказательству plus_n_O. Вместо simpl применим индукцию.

Разберем синтаксис as [| n' IHn']: * Мы указываем Coq имена для переменных в новых целях (subgoals). * Символ | разделяет базовый случай и индуктивный шаг. * В базовом случае (слева от черты) переменных нет, поэтому там пусто. * В индуктивном шаге (справа) мы вводим n' (текущее число) и IHn' (Inductive Hypothesis — индуктивная гипотеза для n').

После ввода этой команды Coq генерирует две цели.

Цель 1: Базовый случай

Здесь нам нужно доказать 0 + 0 = 0. Тактика simpl превращает это в 0 = 0, что очевидно.

Цель 2: Индуктивный шаг

Это самое интересное. Наш контекст выглядит так:

Нам нужно доказать, что S n' + 0 = S n', зная, что n' + 0 = n'.

Сделаем шаг упрощения:

Цель превращается в S (n' + 0) = S n'. Обратите внимание: simpl смог вынести S за скобки, потому что определение plus для аргумента S n' это позволяет.

Теперь мы видим, что внутри S (...) находится выражение n' + 0. А наша гипотеза IHn' говорит, что n' + 0 равно n'. Нам нужно подставить равенство из гипотезы в цель.

Тактика rewrite

Тактика rewrite (переписать) используется для замены одной части равенства на другую.

* rewrite -> H заменяет в цели левую часть равенства из гипотезы H на правую. * rewrite <- H заменяет правую часть на левую.

В нашем случае:

Цель S (n' + 0) = S n' превращается в S n' = S n'. Это тривиальное равенство.

Доказательство завершено! Мы доказали свойство для бесконечного множества чисел, рассмотрев всего два случая.

Индукция для других типов данных

Индукция работает не только для чисел, но и для любых индуктивных типов данных. Рассмотрим списки.

Определение списка

В Coq списки определяются так:

Здесь: * nil — пустой список (аналог O для чисел). * cons — конструктор, добавляющий элемент в начало списка (аналог S). Он принимает элемент типа A и «хвост» (оставшийся список).

!Структура односвязного списка: cons добавляет элемент к существующему списку, а nil завершает цепочку.

Доказательство свойств списков

Принцип индукции для списков звучит так: чтобы доказать свойство для любого списка , нужно:

База: Доказать, что верно.

Шаг: Доказать, что если верно, то тоже верно (для любого элемента ).

Рассмотрим функцию конкатенации (соединения) списков app (часто обозначается инфиксным оператором ++):

Попробуем доказать ассоциативность сложения списков: (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).

Мы делаем индукцию по первому списку l1, так как функция app рекурсивна именно по первому аргументу.

Случай 1: l1 = nil

nil ++ l2 упрощается до l2. Равенство становится l2 ++ l3 = l2 ++ l3.

Случай 2: l1 = cons x l1'

Гипотеза индукции IHl1' утверждает: (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3). Цель: ((x :: l1') ++ l2) ++ l3 = (x :: l1') ++ (l2 ++ l3).

(Здесь :: — это инфиксная запись cons).

После упрощения cons выносится наружу: cons x ((l1' ++ l2) ++ l3) = cons x (l1' ++ (l2 ++ l3)).

Теперь мы можем применить гипотезу индукции, чтобы заменить внутреннюю часть слева на правую часть.

Вложенность тактик

Обратите внимание, что в примерах выше мы использовали маркеры списка - (дефис) для разделения подцелей. В Coq хорошим тоном считается структурирование доказательства. Если внутри одного случая (-) возникает еще одно ветвление, используются маркеры следующего уровня: +, затем *.

Пример структуры:

Заключение

Сегодня мы преодолели важный рубеж. Мы перешли от доказательства простых фактов к доказательству свойств рекурсивных алгоритмов. Мы узнали:

Почему тактика simpl не работает с переменными в рекурсивных позициях.

Как использовать тактику induction для разбиения доказательства на базовый случай и индуктивный шаг.

Как использовать тактику rewrite для применения индуктивной гипотезы (и любых других равенств).

Эти инструменты составляют основу работы верификатора. В следующей статье мы углубимся в логические связки и кванторы, изучив, как доказывать утверждения с «существует» (exists) и «или» (disjunction).

Логика предикатов, зависимые типы и автоматизация доказательств

Мы продолжаем наш курс «Основы формальной верификации в системе Coq». В прошлых статьях мы научились определять функции, работать с пропозициональной логикой (логикой высказываний) и доказывать свойства рекурсивных структур с помощью индукции. Но до сих пор наши утверждения были довольно простыми.

В реальной математике и программировании мы часто говорим не просто «если А, то Б», а делаем утверждения об объектах: «существует такое число , что...» или «для любого списка верно, что...». Это область логики предикатов первого порядка.

Сегодня мы расширим наш арсенал кванторами, прикоснемся к самой мощной концепции Coq — зависимым типам, и, наконец, узнаем, как перестать писать каждое доказательство вручную, доверив рутину автоматическим тактикам.

Кванторы в Coq

Логика предикатов строится на двух китах: кванторе всеобщности («для всех») и кванторе существования («существует»).

Квантор всеобщности (forall)

С квантором всеобщности (forall) мы уже знакомы. В Coq он играет двойную роль: обозначает аргументы функции и логическое утверждение «для всех».

Где — квантор всеобщности, — переменная типа , а — утверждение, зависящее от .

Чтобы доказать такое утверждение, мы используем тактику intros x, которая говорит: «Пусть нам дан произвольный , докажем для него ».

Квантор существования (exists)

Квантор существования утверждает, что в множестве есть хотя бы один элемент, удовлетворяющий условию.

Где — квантор существования, — искомый объект типа , а — свойство, которым этот объект обладает.

В Coq это записывается как exists x : A, P x.

#### Как доказывать существование?

Чтобы доказать утверждение с exists, вы должны предъявить этот объект (свидетеля). Для этого используется тактика exists.

Рассмотрим пример. Докажем, что существует натуральное число, которое больше 10.

Здесь мы явно указали число 42. Coq подставил его вместо , и нам осталось лишь доказать, что .

#### Как использовать существование?

Ситуация меняется, если exists находится не в цели (то, что мы доказываем), а в гипотезах (то, что нам дано). Если мы знаем, что «существует , такой что », мы можем извлечь этот и само утверждение для использования в доказательстве.

Для этого используется тактика destruct.

!Визуализация тактики destruct для квантора существования: из утверждения о существовании мы получаем сам объект и доказательство его свойства.

Зависимые типы (Dependent Types)

Теперь мы подходим к теме, которая делает Coq (и язык Gallina) уникальным. В обычных языках программирования (Java, C++, Python) типы и значения — это разные миры. Тип List не зависит от того, какие числа лежат внутри списка, и уж тем более от их значений.

В Coq типы могут зависеть от значений. Это называется зависимыми типами.

Самый простой пример — это вектор (список фиксированной длины). Тип Vector A n означает «список элементов типа A длиной n». Здесь n — это число (значение), которое является частью типа.

* Vector nat 3 и Vector nat 4 — это разные типы. Вы не можете сложить их или передать в функцию, ожидающую векторы одинаковой длины, без явного преобразования.

Связь с логикой

Почему это важно для верификации? Вспомним изоморфизм Карри — Ховарда:

Утверждение — это семейство типов, индексированное значением .

Доказательство — это функция, которая принимает значение и возвращает объект типа (доказательство для этого конкретного ).

Таким образом, квантор — это и есть конструктор зависимого функционального типа (Dependent Product Type). Когда вы пишете функцию, тип возвращаемого значения которой зависит от входного аргумента, вы используете мощь зависимых типов.

Где — оператор зависимого произведения, — входное значение типа , а — тип результата, зависящий от .

Автоматизация доказательств

До сих пор мы писали доказательства шаг за шагом: intros, simpl, rewrite, reflexivity. Это полезно для понимания, но в больших проектах становится утомительным. Coq предоставляет мощные средства автоматизации.

Тактика auto

Тактика auto пытается решить текущую цель, применяя простые тактики и леммы из базы данных «подсказок» (hints). Она ищет доказательство перебором на определенную глубину (по умолчанию 5).

auto сама сделает intros и apply, найдя путь от гипотез к цели.

Тактика lia (Linear Integer Arithmetic)

Это одна из самых полезных тактик для работы с числами. Она решает задачи линейной арифметики целых и натуральных чисел (сложение, вычитание, умножение на константу, неравенства).

Для использования нужно подключить модуль: Require Import Lia.

Пример, который вручную доказывать долго:

Где — натуральные числа, — строго меньше, — меньше или равно, — импликация.

Если бы мы делали это вручную, нам пришлось бы использовать свойства сложения и неравенств, проводя множество rewrite.

Тактика ring

Если вам нужно доказать алгебраическое равенство, включающее сложение и умножение (например, раскрытие скобок), тактика ring сделает это за вас. Она знает аксиомы кольца (ассоциативность, коммутативность, дистрибутивность).

Где — элементы кольца (например, числа), а равенство следует из свойств операций.

Стратегия использования автоматизации

Важно понимать: автоматизация — это не магия, которая докажет любую теорему. Это инструмент для пропуска рутинных шагов.

Хорошая практика доказательства выглядит так:

Разбейте задачу на подзадачи с помощью induction, destruct или assert.

Упростите выражения с помощью simpl или unfold.

Попробуйте автоматику (auto, lia, easy) для закрытия очевидных ветвей.

Если автоматика не справляется, вернитесь к ручному управлению или добавьте промежуточные леммы.

!Воронка доказательства: от сложной задачи через декомпозицию и упрощение к автоматическому решению.

Заключение

Мы значительно продвинулись в изучении Coq. Теперь вы знаете: * Как формулировать утверждения о существовании объектов (exists). * Что типы могут зависеть от значений, и это фундамент логики Coq. * Как экономить время, используя тактики auto, lia и ring.

Эти инструменты позволяют переходить от учебных примеров к верификации реальных алгоритмов, где ручное доказательство каждой арифметической операции было бы невозможным.

В следующей части курса мы рассмотрим, как извлекать из доказанных на Coq теорем работающий код на языках OCaml или Haskell, превращая верификацию в реальный программный продукт.

Практическая верификация алгоритмов и извлечение сертифицированного кода

Добро пожаловать в заключительную статью курса «Основы формальной верификации в системе Coq». Мы прошли долгий путь: от знакомства с функциональным языком Gallina до автоматизации доказательств с помощью тактик lia и auto. Теперь у нас есть все необходимые инструменты, чтобы ответить на главный вопрос: как применить эти знания для создания реального, работающего и безошибочного программного обеспечения?

В этой статье мы выйдем за рамки учебных примеров. Мы реализуем классический алгоритм сортировки, формально докажем его корректность, а затем превратим наш математический код в исполняемую программу на языке OCaml. Этот процесс называется извлечением кода (code extraction).

Постановка задачи: Сортировка вставками

Для демонстрации мы выберем алгоритм сортировки вставками (Insertion Sort). Он прост в реализации, но его верификация требует нетривиальных доказательств, включающих индукцию и разбор случаев.

Наш план действий:

Написать функцию сортировки на языке Gallina.

Сформулировать спецификацию (что значит «список отсортирован»?).

Доказать, что наша функция удовлетворяет спецификации.

Извлечь сертифицированный код.

Шаг 1: Реализация алгоритма

Сортировка вставками строится на вспомогательной функции insert, которая вставляет число в уже отсортированный список, сохраняя порядок элементов.

Здесь мы используем функцию leb (less or equal boolean), которая возвращает true, если первое число меньше или равно второму. Логика sort проста: мы берем голову списка h и вставляем её в рекурсивно отсортированный хвост sort t.

!Визуализация процесса сортировки вставками: элементы по одному переносятся в результирующий список на свои места.

Спецификация корректности

Написать код — это полдела. Теперь нужно объяснить Coq, что мы от него хотим. Что означает фраза «список отсортирован»?

В математике список отсортирован по возрастанию, если для любых двух индексов и выполняется условие:

Где — индексы элементов, — элемент списка на позиции , а — отношение «меньше или равно».

Однако в Coq удобнее использовать индуктивное определение. Список отсортирован, если:

Он пуст.

Он состоит из одного элемента.

Первый элемент меньше или равен второму, и хвост списка (начиная со второго элемента) тоже отсортирован.

Определим это на языке Gallina:

Это предикат sorted. Если мы сможем сконструировать объект типа sorted l, значит, список l гарантированно упорядочен.

Доказательство корректности

Полная корректность сортировки состоит из двух утверждений:

Результат функции sort является отсортированным списком.

Результат функции sort является перестановкой исходного списка (мы не потеряли и не добавили лишних чисел).

В рамках этой статьи мы сосредоточимся на первом пункте: доказательстве упорядоченности.

Лемма о вставке

Главная сложность скрыта в функции insert. Нам нужно доказать: «Если список отсортирован, то после вставки список insert x l тоже будет отсортирован».

Где — вставляемое число, — исходный список, — предикат упорядоченности, а — логическое следование.

В доказательстве мы используем индукцию по структуре доказательства sorted l. Нам приходится разбирать случаи, когда x меньше головы списка и когда больше. Здесь активно используются тактики simpl (упрощение), destruct (разбор случаев) и леммы арифметики (например, связь leb и <=).

Основная теорема

Имея лемму insert_sorted, доказать основную теорему sort_sorted становится удивительно просто. Мы используем индукцию по списку.

Логика доказательства:

База: sort [] возвращает []. Пустой список отсортирован по определению (sorted_nil).

Шаг: Пусть sort t уже отсортирован (гипотеза индукции IH). Функция sort (h :: t) вычисляется как insert h (sort t). Поскольку sort t отсортирован, мы можем применить нашу лемму insert_sorted, которая гарантирует, что результат вставки тоже будет отсортирован.

Извлечение кода (Extraction)

Мы доказали теорему. В мире математики на этом можно поставить точку. Но в инженерии нам нужна программа. Coq позволяет автоматически транслировать функции из Gallina в языки OCaml, Haskell или Scheme.

Этот процесс называется извлечением. Главная особенность извлечения — стирание типов (type erasure) и удаление логических утверждений.

В Coq есть два мира: * Set / Type — мир данных и вычислений (числа, списки, функции). * Prop — мир логики и доказательств (теоремы, равенства, предикаты).

При извлечении всё, что относится к Prop, удаляется. Почему? Потому что доказательство того, что список отсортирован, нужно только нам (людям и компилятору Coq) для уверенности. Компьютеру для выполнения сортировки само доказательство не нужно, ему нужен только алгоритм перестановки байтов.

!Схема работы механизма Extraction: логические конструкции отбрасываются, оставляя только вычислительное ядро.

Пример извлечения в OCaml

Добавим в конец нашего файла команду:

Coq выдаст нам следующий код на OCaml:

Обратите внимание: в этом коде нет ни следа от sorted, insert_sorted или теорем. Это чистый, эффективный функциональный код. Но у него есть невидимое свойство: он математически гарантированно корректен (в рамках доказанной спецификации).

Доверенная вычислительная база (TCB)

Можем ли мы доверять этому коду на 100%? В формальной верификации существует понятие Trusted Computing Base (TCB) — это набор компонентов, в корректность которых мы вынуждены верить без доказательств.

При использовании Coq в TCB входят:

Ядро Coq: небольшая часть системы, проверяющая доказательства.

Механизм извлечения: алгоритм, переводящий Gallina в OCaml.

Компилятор OCaml: он превращает OCaml в машинный код.

Операционная система и процессор.

Хотя этот список кажется длинным, он на порядки меньше и надежнее, чем при обычной разработке, где мы доверяем еще и миллионам строк кода библиотек, фреймворков и собственной интуиции.

Заключение курса

Мы завершаем наш курс «Основы формальной верификации в системе Coq». Мы прошли путь от простых типов до извлечения сертифицированных алгоритмов.

Что мы узнали: * Gallina — это мощный язык программирования, встроенный в логику. * Типы — это утверждения, а программы — это доказательства (изоморфизм Карри — Ховарда). * Индукция — главный инструмент работы с рекурсивными структурами. * Автоматизация позволяет сосредоточиться на сути задачи, а не на рутине. * Извлечение позволяет перенести гарантии надежности в реальный мир.

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

Спасибо, что были с нами на этом пути. Пусть ваш код всегда компилируется, а доказательства сходятся с первого раза!