3 ms·

I said that they can catch typos. They’re not generally useless, they are just useless with respect to software correctness.

nh2 6y ago
This is evidently false. It is a well-known result of Computer Science how static types and mathematical proofs are equivalent (see https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...). If you make static types sufficiently good, you get a full theorem prover to prove mathematical properties. There is a whole family of modern programming languages used in verification that exploit this; for example, Agda, Idris and Coq are all practical theorem provers built on static types. If you want to go half the way, try Haskell, where you can express slightly less (but still many) correctness requirements with static types, while still maintaining quite easy ergonomics. If you would like to learn more about theorem proving with Haskell in particular, there is an online 3-hour workshop at MuniHac on "Liquid Haskell" in 3 hours (see https://munihac.de/2020.html#programme https://munihac.de/2020.html#programme). It's free and may change your opinion on software correctness significantly.
- amw-zero 6y ago
  You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is one hell of a correspondence and I don’t mean to downplay it at all. But the reason why this isn’t practical in daily programming is that a type represents a set, so all that the isomorphism gets you is knowing that given a member of one type as input you get a member of another type as the output. _Any_ member. This is the problem - the difficulty in verifying logic is showing that the correct output _value_ is given for all input values. Trust me, I have played with Coq for quite a while. Realizing this is what made me abandon the belief that types are some kind of savior. They can be useful, but the program (or proof) itself is what is difficult to get right. I rarely return the wrong type from a function.
  - exdsq 6y ago
    Have you looked into type-driven development? This lets you put your domain model into the type system, potentially add logic if you have dependent types (Idris), and helps a lot with catching issues compared to a dynamic language.
    - amw-zero 6y ago
      Yea and I consider dependent types to be a false idol for the reasons I outlined before. Eventually you just need to compute an arbitrary program within a type check, which is equivalent to just executing the program to begin with.

nh2 6y ago

This is evidently false. It is a well-known result of Computer Science how static types and mathematical proofs are equivalent (see https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...). If you make static types sufficiently good, you get a full theorem prover to prove mathematical properties. There is a whole family of modern programming languages used in verification that exploit this; for example, Agda, Idris and Coq are all practical theorem provers built on static types. If you want to go half the way, try Haskell, where you can express slightly less (but still many) correctness requirements with static types, while still maintaining quite easy ergonomics. If you would like to learn more about theorem proving with Haskell in particular, there is an online 3-hour workshop at MuniHac on "Liquid Haskell" in 3 hours (see https://munihac.de/2020.html#programme https://munihac.de/2020.html#programme). It's free and may change your opinion on software correctness significantly.

amw-zero 6y ago
You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is one hell of a correspondence and I don’t mean to downplay it at all. But the reason why this isn’t practical in daily programming is that a type represents a set, so all that the isomorphism gets you is knowing that given a member of one type as input you get a member of another type as the output. _Any_ member. This is the problem - the difficulty in verifying logic is showing that the correct output _value_ is given for all input values. Trust me, I have played with Coq for quite a while. Realizing this is what made me abandon the belief that types are some kind of savior. They can be useful, but the program (or proof) itself is what is difficult to get right. I rarely return the wrong type from a function.
- exdsq 6y ago
  Have you looked into type-driven development? This lets you put your domain model into the type system, potentially add logic if you have dependent types (Idris), and helps a lot with catching issues compared to a dynamic language.
  - amw-zero 6y ago
    Yea and I consider dependent types to be a false idol for the reasons I outlined before. Eventually you just need to compute an arbitrary program within a type check, which is equivalent to just executing the program to begin with.