я больше говорю о том, что условная скала не надежней условной clojure, но оба эти языка "надежней" других. и истоки этого не в системах типов

Clojure и диалекты Lisp’ов не является полноценным Lambda Calculus’ом …

допустим это правда, но как говорится и чо?

И ничего, просто задачи по преобразованию HList’ов можно делать и в других языках… и вокруг них строить формальные абстракции и доказать корректность во время компиляции.

Как формально верифицировать Clojure ?

а можно этого не делать и получать работающие программы

Работающие и корректные - разные вещи.

Просто в Clojure тоже есть свои примитивы для Referential transparency, и свои функциональные структуры для свободных вычислений… просто называются по другому, и не следуют формальному набору законов.

скомпилированная и корректная - разные вещи. Вы будете утверждать, что программы на скале в целом надежней программ на clojure?

Тут момент в том что некорректная - не компилируется…

Clojure - repl driven development, что имеет свой ряд ограничений и особенностей разработки.
Опять же я не представляю чем можно верифицировать программу на Clojure.

Я, лично, спокойно пишу и на Clojure, и на Scala и на Kotlin’e… потому мне проще судить о состоянии соответствующих решений.

Ну тогда у вас наверное есть понимание, что не система типов делает программу надежной?

Систему типов тоже нужно формально верифицировать для этого.
В случае со скалой есть конкретный инструментарий и принципы тестирования формальных законов.
В котлине их нет из-за негибкой системы типов…
В кложуре - дальше дизайна стандартной библиотеки дело не доходит, можно формально верифицировать всё что более-менее referentially transparent, но ряд side effect’ов просто игнорируется.

То есть вы перед началом работы полностью строите систему типов для  проекта, верифицируете и до сдачи проекта она не меняется? Я такое могу представить только если я буду калькулятор писать

Существующие законы и тесты для верификации уже написаны и являются частью соответствующих библиотек.
Да, для любой задачи есть своя система типов и свои принципы обхода иерархий этих типов (если это HList )- это основа generic программирования.

Ну там к примеру есть те же Refined Type’ы

И можно написать что-то типа

val i1: Int Refined Positive = -1

и оно отвалится при компиляции

То есть вы и в скале своих типов не создаете, а обходитесь уже существующими?

По большей части да, но если и пишутся свои типы - это очень сложные и специфические задачи.
Раз в 2-3 года точно.

клево, я бы посмотрел на такую систему, есть что-то такое в опенсорсе?

скажите а что вы думаете насчет Elixir?

Ну «он есть».
Практическая польза тоже есть, но есть ряд задач для которых он просто неприменим.

Если стоит задача писать что-то высокодоступное - лучше сразу идти в Rust и системное программирование с использованием соответствующих подходов к Highload’ам…
Даже на golang’e с sync.Pool’ами объектов и zero-alloc подходами можно писать очень быстрые вещи (с выключенным GC), но это подходы почти полностью состоящие из хаков и переписывания stdlib'a.

это просто самый первый язык который выскакивает при упоминании fp

Лучше бы уже сразу хаскель выскакивал ...