Вон Compcert компилируется, а ошибки в нём до сих пор находят.

>тесты делают то же самое
Нет, тесты подтверждают правильное поведение программы только на определенных входных данных. А здесь мы можем быть уверены что если теорема написана правильно, то программа будет работать на всех входных данных.
>А какой смысл писать ...
Перестраховка. Написал два раза, и можешь быть уверен что если программа скомпилировалось, то ты не поставил там по пьяни другой знак. Ну или ты совершил одинаковую ошибку в коде и пруве, но я не знаю кем нужно быть чтобы такое совершить.
>Чтобы я видел что здесь можно вызвать undefined
В нормальных языках с сильной системой типов нет undefined
>Недавно фигачил в марафонском режиме...
Можешь не использовать прувы. Но в таком случае практически всегда в программе будут баги, так как тесты не могут покрыть весь код и все возможные варианты данных.

Ну гарантию что ты не совершишь ошибку тебе никто не даёт. Просто ее шанс минимизируется.

А вы сами пробовали что-нибудь нетривиальное в coq, agda, f* или idris формализовать?

Нетривиальное пока нет

Фраза про "на одну строчку кода приходится 50 строк доказательств" не просто так появилась)

Ну, это преувеличение. От 5 до 10 строчек ;)

Хз, вроде в докладах часто мелькает именно число 50, хотя это конечно число навскидку))

Это если одну тактику на строке писать ;)
Надо сказать, что 5 строк доказательств на одну строку кода — это такой уровень, над которым приходится трудиться изо всех сил.

Обычно на одну строку кода ноль строк доказательств?

Это если одну тактику на строке писать ;)
Надо сказать, что 5 строк доказательств на одну строку кода — это такой уровень, над которым приходится трудиться изо всех сил.

Тем не менее, они покрывают. Я могу доказать в конкретно своём случае, что из корректности на предоставленных тестах следует корректность на любом тесте (конечно, с учётом синтаксиса алгоритма). Я думаю, в общем случае, это какое-то следствие PCP-теоремы, если алгоритм достаточно "гладкий", допустим, в терминах информационных систем Скотта, то его можно гарантированно тестить малыми объёмами тестов.

Вот и вопрос: а должен ли я заставлять своего пользователя трудиться над этим? Оно понятное дело, что дело очень интересное. Но вот есть у меня друг - биолог, ему важнее пересчитать варианты (забыл научное название) кусочков форм вирусов уже сейчас, потому как через год уже будет другой штамм гриппа...

А я вот не понимаю, есть ли вообще надежда, что когда-нибудь с типами будет легко и просто доказываться всё. А ещё лучше, будут ли завтипы выводится? Или это вообще невозможный вариант?

А в каком направлении становится лучше? Может, есть обзор какой-нибудь того, куда всё движется?

А в каком направлении становится лучше? Может, есть обзор какой-нибудь того, куда всё движется?