Using haskell as my main language at work is pretty great, except for one thing. Having learned agda first, I got really used to having dependent types at my disposal. Now I often find myself naturally thinking of a solution that makes use of dependent types, then having to translate this solution into haskell. Of course, there is always a translation. But the translation may obfuscate what the code is doing, making it harder for future programmers to understand it and maintain it.
The work I do has no relation to formal verification, nor is it "mission critical" that the code is correct. But I still find my self wishing I could use dependent types, just because they make writing programs and capturing business logic both faster and easier. A language with dependent types requires a less severe translation from the programmers ideas to a compiling program.
=> More informations about this toot | More toots from isAdisplayName@mathstodon.xyz
@isAdisplayName I can’t stand the PR campaign in programming languages that our stuff is only (or even especially!) good for “mission critical” programming. it’s the human parts that matter
=> More informations about this toot | More toots from chrisamaphone@hci.social
@chrisamaphone @isAdisplayName I don't think the PR campaign would exist if we just had a wealth of funding to research what we wanted. But funding is scarce and competitive and we have other parts of computer science claiming they're about to solve general AI
Like the committee for Canada's main science grants have zero PL people on it. Thankfully they get external reviews.
=> More informations about this toot | More toots from joey@mathstodon.xyz
text/geminiThis content has been proxied by September (3851b).