Formeel bewijsbare programmeertalen zijn gewoon een esoterisch idee uit de wiskunde / informatica dat niet goed vertaalt naar de echte wereld. Ze schalen simpelweg niet voor praktische code. De realiteit is dat als je een succesvol ontwikkelaars-ecosysteem wilt opbouwen, je taal meer moet lijken op JavaScript dan op Haskell. Dit is vooral waar met de opkomst van LLM's, waar talen met meer trainingsdata hun marktaandeel blijven vergroten. Ik zeg dit als iemand wiens favoriete programmeertaal Haskell was en die deze systemen van begin tot eind heeft ontwikkeld, van het ontwerp van de taal tot de compilers, en zelfs de onderliggende wiskundige oplosser. Ze schalen niet omdat de onderliggende wiskundige oplosser exponentieel explodeert.