Conversation

Oh god, this bullshit again. There is ZERO evidence that any type checker less powerful than Coq will catch more bugs than being healthy and well-rested. If you use Haskell but eat junk food and don't exercise, then you're unethical. twitter.com/PttPrgrmmr/sta

This Tweet is unavailable.

123

341

swann

@evertedsphere

Jul 17, 2018

I usually enjoy it when you take this line, but what makes Coq uniquely powerful here? What's the (Sorites-like) line that divides the "actually catch bugs" type systems from the "McDonalds and Netflix" type systems? 1/

swann

@evertedsphere

Jul 17, 2018

Haskell will get dependent types in a few years (one of this year's GSoC projects is replacing the Core language with one that supports them, as proof that there's work happening here). What then? 2/

Paolo G. Giarrusso

@Blaisorblade

Jul 17, 2018

As Chlipala shouts from rooftops, dependent types have limited relevance, proof automation matters far more, and Haskell only gets (unsound) dependent types; they’ll help with certain invariants but aren’t enough to (feasibly) prove full functional correctness.