А какой смысл писать result = a - b, если  и так написано substract a b = a - b? Ведь, чисто с технической точки зрения, мы просто увеличиваем корректность кода повторением одного и того же в двух разных местах. Но, ведь, нет никаких гарантий, что ошибка именно на уровне типов, а не на уровне термов. Во-вторых, тесты делают то же самое. И можно строго доказать, что не нужно проверять каждую функцию в программе, а достаточно проверять свойства на верхнем уровне, и тогда с высокой степенью вероятности substract будет вести себя, как -.

Прошу прощения за offtopic, но для меня этот вопрос животрепещущий в дизайне языка, поэтому я задаю все эти глупые вопросы. То есть, я не противник полезности типов, но мне бы хотелось понять истинную их ценность.

Я вот недавно фигачил в марафонском режиме математический код на Схеме (сам не знаю, как так получилось), задача про bigdata, и структуры данных там были не самые тривиальные. Ошибки в типах при этом были редким явлением и совсем примитивное тестирование их обнаруживало сразу же. Основные ошибки были в самих вычислениях, даже в самой математической модели. И если бы мне пришлось всякий раз менять систему доказательств (даже если принять, что я мог бы выразить всю нужную мне математику в типах), я бы и за год не справился бы с этой задачей. Это можно утверждать наверняка, потому что есть же пример Certigrad,  где для обоснования простого градиентного спуска потребовалась годовая работа института. Хотя, на бумажке это делается минут за 15.

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

Или нет? Что я не вижу, не замечаю и игнорирую?

Не только повторением, но и тем, что у языка спецификации другое предназначение, поэтому в нём a-b имеет математический смысл и не может переполниться. Поэтому в данном примере система доказательств укажет на несоответствие кода спецификации и исполняемого кода, даже если вам очевидно, что там всё правильно и незачем повторяться. Соответственно, придётся принять меры - либо сузить входные значения, либо расширить выходное. А в тестах вы узнаете, утрировано, что 4-2=2. Конечно, можно постараться и написать тесты гораздо лучше, только объём их и сложность будет несоизмеримо больше спецификации, а гарантий давать они будут по-прежнему меньше.
Так как я веду речь не о зависимых типах в языке, а о формальных спецификациях вообще, то их использование может никак не сказываться на сложности и скорости создания кода. Если полное доказательство слишком дорого, то спецификации можно использовать для тех же тестов, генерируя по ним проверочный код, как это делает, к примеру, E-ACSL plugin Frama-C

Что я не вижу, не замечаю и игнорирую?
А попробуйте подумать не о том, как это Вам может помешать, а о том, как это может Вам помочь.

Ну... Я пока не вообще о формальных методах, а именно о теории типов. Теория типов даст 99.9999% гарантию, если - реализован, как операция на индуктивных типах. А если - аксиоматический, зависит от реализации и т.д. и т.п. То степень гарантированности снижается.

Тест же тестирует именно то поведение системы, каким она себя проявляет в реальности. Ну, и я настаиваю, что нет никакой целесообразности тестировать поведение функции substract.   Тестировать надо более крупные блоки кода. Если функция обращения матриц обращает случайную матрицу корректно, то вопрос: какова вероятность того, что мой минус написан неправильно?

И вопрос: а как долго я буду доказывать, что обращение матриц правильно работает на float-ах? Смогу ли я доказать корректность сложного алгоритма? Или мне придётся ограничится упрощённым и медленным? Насколько эффективным будет извлечённый из доказательства код? Вот в seL4 извлечённый код руками и скриптами на Bash подправляют.

Тут много технологических вопросов.

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

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

Так я нашёл. Certigrad, MLCert, seL4. Объёмы доказательств удручают

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

А мою реплику про неполное доказательство Вы не увидели?

А спецификации - это очень компиляторная тема. Компилятор может улучшить статический анализ ошибок и найти дополнительный источник информации дял оптимизации.
Так пойдёт?

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