4 ms·

> Actually, if your type system is powerful enough, you don't need to test. That's the source of the "if it compiles, 99% of the time it works right" people men

> Actually, if your type system is powerful enough, you don't need to test. That's the source of the "if it compiles, 99% of the time it works right" people mention about Haskell (and even more so languages like Idris etc). Types only eliminate certain tests. You will always have system tests, acceptance tests and unit tests. One should use types to augment their system reliability. Types will not catch logical errors in your code.

coldtea 7y ago
>Types only eliminate certain tests. You will always have system tests, acceptance tests and unit tests. Yes, so let's eliminate them with types, instead of doing them. "Acceptance tests" are not concerned with programming. >Types will not catch logical errors in your code. Actually, depending on the type system, it will. That's how program logic is tested as "proof" and programs, implementations of algorithms are determined to be logically correct in more exotic languages (but even in C + some restrictions + the right statically checking tooling, NASA/JPL style project do that). https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification
- pfdietz 7y ago
  The question is not whether a type system will catch bugs. The question is whether a type system finds enough bugs that tests (sufficient to cover the things that the type system does not catch) would not also catch. If you have to point to something like Idris I don't think you're making a real world argument yet.
verttii 7y ago
Haskell's type system most definitely does catch some of your logical errors. That's exactly why it is so revered. An effective use of a type system such as Haskell's Hindley-Milner can result in a vastly smaller surface area for possible problems and thus can cut a big number of otherwise mandatory unit tests off your todo list.

coldtea 7y ago

>Types only eliminate certain tests. You will always have system tests, acceptance tests and unit tests. Yes, so let's eliminate them with types, instead of doing them. "Acceptance tests" are not concerned with programming. >Types will not catch logical errors in your code. Actually, depending on the type system, it will. That's how program logic is tested as "proof" and programs, implementations of algorithms are determined to be logically correct in more exotic languages (but even in C + some restrictions + the right statically checking tooling, NASA/JPL style project do that). https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification

pfdietz 7y ago
The question is not whether a type system will catch bugs. The question is whether a type system finds enough bugs that tests (sufficient to cover the things that the type system does not catch) would not also catch. If you have to point to something like Idris I don't think you're making a real world argument yet.

verttii 7y ago

Haskell's type system most definitely does catch some of your logical errors. That's exactly why it is so revered. An effective use of a type system such as Haskell's Hindley-Milner can result in a vastly smaller surface area for possible problems and thus can cut a big number of otherwise mandatory unit tests off your todo list.