Сила Coq не в ядре, а в библиотеке доказанных лемм
Вопрос «сколько правил нужно ядру» — правильный инстинкт с неверной единицей измерения.
| Coq / Lean | flang | |
|---|---|---|
| Правил вывода в ядре | ~15–20 | 11 |
| Тактик (автоматика, ядру не доверяет) | ~200 | 0; вместо них один недоверенный поиск |
| Доказательство пишется руками | да, терм или тактика | да, теорема в духе Isar: 160 в дереве, 53 в flang/stdlib |
| Готовых доказанных утверждений | десятки тысяч; в Lean mathlib за 200 000 | 407 |
(Числа по Coq и Lean — по памяти, порядок верный, точность до десятков не гарантирована. Числа flang мерены: правила — grep -c 'тотальная функция «Правило' flang/self/proof-kernel.flang; теоремы — grep -rc '^\s*теорема ' flang --include=*.flang; доказанные утверждения — утверждения.доказано в docs/site/numbers.json.)
Маленькое ядро — это гордость, а не недостаток: доверять надо малому куску, чем ядро меньше, тем меньше места для ошибки. Разрыв по правилам не в порядках.
Третья строка — не разрыв, а совпадение, и путать её с разрывом дорого. Механизм Coq у flang есть: цель, шаги, обоснование каждого шага, ядро только сверяет. Противопоставление «там доказательство пишет человек, а тут машина» ложно — оно опровергается одним грепом. Верное различие тише: у flang к тому же механизму приделана автоматика, и часть утверждений закрывается без единой написанной строки — вердикт печатает это отдельным числом (утверждений 177: доказано 114 … из них без теоремы 54 — замер на flang/stdlib/sha1.flang с импортами).
Настоящий разрыв — в последней строке. В Coq никто не доказывает с нуля: берут готовую лемму и опираются. Это накоплено за тридцать лет сотнями людей, и никакое правило ядра этого не заменит.
Порядок работ, от важного к неважному:
- научить язык говорить условные факты — unstatable-costs-more-than-unprovable;
- набрать библиотеку лемм — но не десятки тысяч, а те, которых требует наш корпус;
- добавлять правила в ядро — наименее важное, см. the-bottleneck-is-rule-strength.
Связано: zero-axioms, condition-for-the-revolution