Проблема в том, что рассматриается вырожденный случай, когда всем всё понятно, что правильно
А этот очевидный случай как раз неправильный и система доказательства полной корректности бы его не приняла.
Ну и вполне нормально написать в спецификации что result = a - b, а не городить всё то, что тут было предложено
А какой смысл писать result = a - b, если и так написано substract a b = a - b? Ведь, чисто с технической точки зрения, мы просто увеличиваем корректность кода повторением одного и того же в двух разных местах. Но, ведь, нет никаких гарантий, что ошибка именно на уровне типов, а не на уровне термов. Во-вторых, тесты делают то же самое. И можно строго доказать, что не нужно проверять каждую функцию в программе, а достаточно проверять свойства на верхнем уровне, и тогда с высокой степенью вероятности substract будет вести себя, как -.
Прошу прощения за offtopic, но для меня этот вопрос животрепещущий в дизайне языка, поэтому я задаю все эти глупые вопросы. То есть, я не противник полезности типов, но мне бы хотелось понять истинную их ценность.
Я вот недавно фигачил в марафонском режиме математический код на Схеме (сам не знаю, как так получилось), задача про bigdata, и структуры данных там были не самые тривиальные. Ошибки в типах при этом были редким явлением и совсем примитивное тестирование их обнаруживало сразу же. Основные ошибки были в самих вычислениях, даже в самой математической модели. И если бы мне пришлось всякий раз менять систему доказательств (даже если принять, что я мог бы выразить всю нужную мне математику в типах), я бы и за год не справился бы с этой задачей. Это можно утверждать наверняка, потому что есть же пример Certigrad, где для обоснования простого градиентного спуска потребовалась годовая работа института. Хотя, на бумажке это делается минут за 15.
Вот и вопрос... А язык я делаю именно для таких нагрузок (ну, то есть, получается, под себя и коллег). По идее, мне нужен не такой инструмент, который заставляет меня повторять в очень сложном формализме все мои алгоритмические заморочки, а такой, который по коду предсказывает возможные проблемы в исполнении. Чтобы я сразу видел, что вот тут есть шанс вызвать #undefined, как функцию, и вот тебе тестовый контрпример.
Или нет? Что я не вижу, не замечаю и игнорирую?
