3 ms·

So where does it fall down? Excluding the social ones I mentioned.

• tome 9y ago
  Can you prove the correctness of a sort function in the type system? I don't know any mainstream language where you can do that. You'd have to go to something like Agda, Idris, Coq or F* which are hardly practical languages (currently). Beyond that there's an entire universe of complexity that we have no idea how to prove (practically) in the type system. Haskell types encode simple properties. They're extremely useful properties in practice but they don't come anywhere near "everything" we would want to prove.
  • open_bear 9y ago
    What do you think about clojure.spec approach?
    • empthought 9y ago
      Those aren't proofs at all, and the docs even say so.