Les langages de programmation formellement prouvables ne sont qu'une idée ésotérique en Mathématiques / Informatique qui ne se traduit pas bien dans le monde réel. Ils ne sont tout simplement pas évolutifs pour un code pratique. La réalité est que si vous voulez construire un écosystème de développeurs réussi, votre langage doit ressembler davantage à JavaScript qu'à Haskell. Cela est particulièrement vrai avec la montée des LLM, où les langages avec plus de données d'entraînement continueront à accroître leur part de marché. Je dis cela en tant que personne dont le langage de programmation préféré était Haskell et qui a développé ces systèmes de bout en bout, de la conception du langage aux compilateurs, et même aux solveurs mathématiques sous-jacents. Ils ne sont pas évolutifs car les solveurs mathématiques sous-jacents explosent de manière exponentielle.