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 argu

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