3 ms·

> These tests only cover the type space, which is trivial. Granted it's not enormous, but if you think it's trivial you'll probably be surprised by the range o

• kazinator 10y ago
  That encoding requires you to be a type system expert, and write reams of additional code surrounding the actual code. That additional code has to be well thought out and designed; proofs don't just pop out of thin air, all ready to go and represented as type via Curry-Howard! Ordinary code does not encode very interesting things about itself via its typing. Well typed usually just means "there is no trivial mistake here", on about the same level as a missing semicolon in a C struct declaration.
  • dllthomas 10y ago
    That's just not true. I have some interest in types (mostly practical, some theoretical) but I have no graduate degree, I still regularly encounter both theory and type voodoo I don't understand, and I wouldn't consider myself a "type system expert". On a recent project I was able to use the type checker to help me catch things including 1) passing a bid price where I meant an ask price, 2) using an index into the wrong array, 3) calling a function not permitted to run on the thread in question (because of data access or deliberate marking). This wasn't Haskell - it was C.