>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).
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.
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