u/matt-noonanin r/haskell • Recommends
On “Dependent types: A pessimist debates an optimist on Hacker News”
…e systems and I like FP, but pron is pretty much 100% on target with this comment. I think it is really worth taking a step back to understand what he is saying here. We could do so much better.
>Not only do I not dislike type theory vehemently, I really like some of its uses (like linear types; don't believe me? I praised them in a recent talk: [video I'm not too fond of deductive proofs as a software verification method because so far it manages to scale worse than other formal methods (that don't scale that well, either). What I strongly dislike is:
>
>1. Fetishization of certain formalisms, particularly combined with a rather limited understanding of said formalisms or formal syst…