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

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

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

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

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

Поскольку генерируется код, а не бинарник, изучать его всегда можно. Некоторым-то и бинарник не проблема. 😊
Другое дело, что этот код ничем человеческий не напоминает.

А вот этого нельзя - чекер не пропустит... Можно сделать ошибку в типах/спецификации, но вот в доказательстве - нельзя.

Fortress? 😉

Я не про семантические офибки, а скорее логических, например не полностью ограничения, некорректные условия, ошибки / неточности в спецификации. Ну и все что можно отнести к категории математического софизма.

Всё-таки ошибки в спецификации и ошибки в доказательстве - две большие разницы. И пафос machine-checked доказательств в том, что компьютер не пропускает "софизмы" и прочий handwaving.

Интерестно, убежет ли она от «ошибки Эйлера»?) Я про 1 == -1
1  =>  √1 => √(-1)*(-1) => √-1 * √-1 => i * i => -1

? =)

но ведь ошибки можно допустить и при написании самих пруфов;)

Интерестно, убежет ли она от «ошибки Эйлера»?) Я про 1 == -1
1  =>  √1 => √(-1)*(-1) => √-1 * √-1 => i * i => -1

? =)

А пачку условий, если левый и / или правый меньше 0?

Убережёт. Будет в типе sqrt записано, что требуется x >= 0.

Значит у тебя код в 99% случаев не скомпилируется

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

Это комплексные числа

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

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

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

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

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

Такое пытаются делать в mini kanren