Type annotations are not comparable to unit tests at all. Unit tests verifies correctness of the behavior, not just the types. E.g. if you have a mathematical function like min(), unit tests can verify it return the smallest of the inputs. Type annotations can at best verify that it returns a value of the same type as the input, but not if it is the smallest, largest or something random.
Type annotations are great for documentation and as a basic sanity test. They are especially useful with tools like code analysis or refactoring tools. But types are is no way a substitute for unit tests.
It tests at compile time that some function f takes A and returns B. That covers 99% of all possible input/output which you technically have to do in an untyped language. How do you make sure your function that takes an `any` doesn't crash and burn or silently sneak through and write null to the database?
> It tests at compile time that some function f takes A and returns B. That covers 99% of all possible input/output which you technically have to do in an untyped language.
Sorry, I don't understand what you are saying here. By A and B are you referring to the correct output given an input, or just to the expected data type? Because there is a big difference, as with the `min()` example.
yes because the set of possible inputs for A -> C is basically infinite. But min(A,B)=C is only 2^64^2. Why shouldn't you test for string, object, object of object, object with a certain kind of shape, or Number class as opposed to number primitive? How can you know it will or won't work from a unit test perspective?
But the purpose of unit tests is to show that the code under test is correct, i.e. that min() return the smallest input, not just a random value of the same type. Static typing cannot do that, so it is in no way a substitute for unit tests.
Static typing is a useful tool, just not a substitute for any unit tests. The risk of static typing is when it becomes a goal in itself and you start thinking correctness means the program satisfies the type checker.
One possible answer is that you make that a feature: the database can contain null, and it means something. In some cases you will trade one problem for another, but the economics of the tradeoff in overall productivity can be favorable.
That very much depends on the type system you use. With (for example) refinement types and dependent types you can prove your code correct with zero tests needed. Examples are F*, Idris, Agda, Coq etc.
Prove the code is correct per the design, it doesn’t eliminate the possibility of design errors which can still benefit from tests (or QuickCheck like tools) to ensure that what you design does what you think it does … a critical component given how rarely you see these languages used to actually build large applications in the wild.
The key difference is that with proven correct code you actually have a formal spec you can prove properties about. Without proven correct code you don’t even have a formal spec. Just a bunch of random tests (if you are lucky) that may or may not match your informal spec.
And the argument that if you can’t prove your design correct then there is no point proving your code correct is a strange one. That’s like saying that there is no point writing tests because you can’t prove your design correct or guarantee that all tests needed will be written. Ehhhh nope. I have written and generated more than 9000 tests for a very large scale C++ applications that are used by large corporations around the world. And I haven’t had a bug in production for 5+ years. However I of course can’t prove that those tests cover everything or that my design is correct. But that doesn’t mean it isn’t worth doing.
Yeah, I feel way too many people mistake "we can't cover 100% of everything" with "it's not worth tightening the bolts". Strange conflation but a very common one indeed.
All well-formed code is always a correct version of itself (Curry-Howard correspondence). It's just that sometimes you thought it was a correct version of something else and turn out to be wrong about that.
Since dependent type systems are just another kind of code, this is still true.
Type annotations are great for documentation and as a basic sanity test. They are especially useful with tools like code analysis or refactoring tools. But types are is no way a substitute for unit tests.