Idris: A Language for Type-Driven Development

Re:Idris: A Language for Type-Driven Development by still_grokking on Saturday January 21, 2023 @02:49AM (#34464715)

> There's a reason languages like Idris, Haskell and so forth are much more popular in solipsistic domains like theorem-proving than they are in a business application.

Scala developers would disagree.

Especially in business applications strong static types are extremely helpful to prevent bugs and model the domains of interest in a proper way.

[ Parent | on HN ]

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

[ Parent | on HN ]