4 ms·

The part about static types is weird. "Tests are not always perfect but can be useful. However static types are not perfect and so they are useless."

amw-zero 6y ago
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.
carlmr 6y ago
I had the same reaction. Static types can provide very good constraints, obviating a lot of testcases, also they provide a lot of implicit interface documentation when done well. I really like this talk: https://fsharpforfunandprofit.com/ddd/ https://fsharpforfunandprofit.com/ddd/
- KingOfCoders 6y ago
  I've used a lot of tag types in scala to document and constrain interfaces and liked it a lot.
fgonzag 6y ago
I felt the same about it. Static typing is a tool, just like unit testing, integration testing, and code reviews. We combine these tools in order to maximize software quality, ease of development and maintenance. Static typing eliminates a whole class of errors that good code bases in dynamic languages usually have to manually test (instance and type tests)
- amw-zero 6y ago
  There is no need to have “type” tests in dynamically typed languages. Dynamically typed objects are implementation details, you test without referring to the underlying types. Also, static types _are_ manual testing, you need to write the types.

amw-zero 6y ago

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.

carlmr 6y ago

I had the same reaction. Static types can provide very good constraints, obviating a lot of testcases, also they provide a lot of implicit interface documentation when done well. I really like this talk: https://fsharpforfunandprofit.com/ddd/ https://fsharpforfunandprofit.com/ddd/

KingOfCoders 6y ago
I've used a lot of tag types in scala to document and constrain interfaces and liked it a lot.

fgonzag 6y ago

I felt the same about it. Static typing is a tool, just like unit testing, integration testing, and code reviews. We combine these tools in order to maximize software quality, ease of development and maintenance. Static typing eliminates a whole class of errors that good code bases in dynamic languages usually have to manually test (instance and type tests)

amw-zero 6y ago
There is no need to have “type” tests in dynamically typed languages. Dynamically typed objects are implementation details, you test without referring to the underlying types. Also, static types _are_ manual testing, you need to write the types.