Re:Idris: A Language for Type-Driven Development
by ykonstant on Saturday January 21, 2023 @03:29AM
(#34464868)
I agree; I would expect to see such languages feature much more prominently there, especially in the subtle and convoluted business/legal complex.
One may argue that the proof-strength formality can be a hindrance: in such domains, inconsistencies and contradictions abound, and some of them cannot be predicted in advance. But I believe that languages like Idris can accommodate this. Maybe I am wrong, or maybe they can, but not more efficiently than more free-form languages.
...but ok, I am failing to see what I can do with COBOL that I cannot do with Idris, business-logic-wise. lol
One may argue that the proof-strength formality can be a hindrance: in such domains, inconsistencies and contradictions abound, and some of them cannot be predicted in advance. But I believe that languages like Idris can accommodate this. Maybe I am wrong, or maybe they can, but not more efficiently than more free-form languages.
...but ok, I am failing to see what I can do with COBOL that I cannot do with Idris, business-logic-wise. lol