Формально доказуемые языки программирования — это просто эзотерическая идея из математики и информатики, которая плохо переводится в реальный мир. Они просто не масштабируются для практического кода. Реальность такова, что если вы хотите создать успешную экосистему разработчиков, ваш язык должен быть больше похож на JavaScript, чем на Haskell. Это особенно верно с ростом LLM, где языки с большим объемом обучающих данных будут продолжать увеличивать свою долю на рынке. Я говорю это как человек, чей любимый язык программирования был Haskell и который разработал эти системы от начала до конца, от проектирования языка до компиляторов и даже до базовых математических решателей. Они не масштабируются, потому что базовые математические решатели взрываются экспоненциально.