Linguagens de programação formalmente prováveis são apenas uma ideia esotérica de Matemática / Ciência da Computação que não se traduz bem para o mundo real. Elas simplesmente não escalam para código prático. A realidade é que, se você quer construir um ecossistema de desenvolvedores bem-sucedido, sua linguagem precisa ser mais parecida com JavaScript do que com Haskell. Isso é especialmente verdadeiro com a ascensão dos LLMs, onde linguagens com mais dados de treinamento continuarão a aumentar sua participação de mercado. Digo isso como alguém cujo idioma de programação favorito era Haskell e que desenvolveu esses sistemas de ponta a ponta, desde o design da linguagem até compiladores, e até mesmo os solucionadores matemáticos subjacentes. Eles não escalam porque os solucionadores matemáticos subjacentes explodem exponencialmente.