Революция наступит ровно тогда, когда доказательство станет дешевле тестов

Закрыть список задач к 1.0.0 — значит догнать существующее. Модульная система есть у всех, пакетный менеджер есть у всех, лёгкие процессы есть у Erlang. Получится хороший язык, каких за двадцать лет вышло штук тридцать, и почти все умерли не потому, что были плохи.

Условие, при котором это становится чем-то большим, одно и оно измеримо:

Доказать функцию должно стоить дешевле, чем написать на неё тесты.

Сегодня в мире доказательство стоит в 5–20 раз дороже тестов, поэтому доказывают только ядра ОС, криптографию и авионику. Все знают, что зависимые типы мощные; никто не сделал их дешёвыми. Это и есть открытая задача — а не «сделать ещё один функциональный язык».

Если цена упадёт ниже цены тестов, меняется не язык, а то, что делают программисты: доказательство пишется один раз и покрывает все входы, тесты пишутся вечно и покрывают те, до которых додумались.

Измерено, и ответ жёсткий. Замер сделан: двадцать обычных функций библиотеки, на каждую написаны и тесты, и доказательство. Результат — 0 из 20 доказано, при четырёх настоящих ошибках, найденных тестами. Подробно: proof-cost-0-of-20.

То есть говорить «дешевле или дороже» пока рано: доказать обычную функцию библиотеки сегодня нельзя вообще. Причина названа и она чинится — no-induction-for-builtin-types.

Вторая половина вопроса — цена доказуемости в работе программы — тоже измерена, и она почти нулевая: 2,5 % функций, а счётчики шагов вообще внутри разброса прибора (provability-costs-2-5-percent). То есть дорого стоит написать доказательство, а не иметь его. Это разные цены, и путать их нельзя.

Три исхода, а не два: ядро доказало само (цена ноль), пришлось писать теорему (цена есть), не вышло — и здесь отдельно «правил не хватает» против unstatable-costs-more-than-unprovable.

Связано: proof-cost-0-of-20, the-bottleneck-is-rule-strength, coq-strength-is-in-its-lemmas