Formellt bevisbara programmeringsspråk är bara en esoterisk Math / CS-idé som inte översätts bra till den verkliga världen. De skalar helt enkelt inte för praktisk kod. Verkligheten är att om du vill bygga ett framgångsrikt ekosystem för utvecklare måste ditt språk vara mer likt JavaScript än Haskell. Detta gäller särskilt med framväxten av LLM:er, där språk med mer träningsdata kommer att fortsätta att öka sin marknadsandel. Jag säger detta som någon vars favoritprogrammeringsspråk var Haskell och som har utvecklat dessa system från början till slut, från språkdesign till kompilatorer och till och med de underliggande matematiska lösarna. De skalas inte eftersom de underliggande matematiska lösarna exploderar exponentiellt.