But, crucially, the things a test checks don't generalize.
I think this is the most important thing to note. When I say
Example test_fac1: (factorial 3) = 6.
Proof. reflexivity.
This is completely different from the statement
Theorem eq_fac : forall (n : nat),
fac n = prod 1 n
Tests are simply a mathematical proof of a relation on a specific subset of the domain and codomain of the function. Types, in the broad sense, are constrained proofs over the properties of all elements in the domain and codomain.
Types are useful -- they're perhaps the greatest success of formality in software engineering ever. However, they're not complete and completeness is hard. Types succeed because they provide a lot of benefit for very little pain (the constraints you discuss in your post). Your assertion is simply reinforced when we look at the other classes of correctness that we could guarantee. We could write fixpoint definitions for all functions which require structural recursion. We could push all side effects to typed lambda calculus sugar.
Fundamentally, we could prove our code correct. But that's a pain in the ass. And it still doesn't work. Tests complement proofs -- they ensure that our own conception of the definition fits our expectations. We could do all the work to formally prove our conjectures, but if our definitions were wrong the conclusions would be useless.
What I'm saying is that all of these things should work together -- and the result is a balancing act. We want additional guarantees that our programs are correct, but it requires us to program differently because only certain types of programs have the properties that we wish to exploit. The benefit is that we do have this additional information, so I agree that we should use it.
I think this is the most important thing to note. When I say
This is completely different from the statement Tests are simply a mathematical proof of a relation on a specific subset of the domain and codomain of the function. Types, in the broad sense, are constrained proofs over the properties of all elements in the domain and codomain.Types are useful -- they're perhaps the greatest success of formality in software engineering ever. However, they're not complete and completeness is hard. Types succeed because they provide a lot of benefit for very little pain (the constraints you discuss in your post). Your assertion is simply reinforced when we look at the other classes of correctness that we could guarantee. We could write fixpoint definitions for all functions which require structural recursion. We could push all side effects to typed lambda calculus sugar.
Fundamentally, we could prove our code correct. But that's a pain in the ass. And it still doesn't work. Tests complement proofs -- they ensure that our own conception of the definition fits our expectations. We could do all the work to formally prove our conjectures, but if our definitions were wrong the conclusions would be useless.
What I'm saying is that all of these things should work together -- and the result is a balancing act. We want additional guarantees that our programs are correct, but it requires us to program differently because only certain types of programs have the properties that we wish to exploit. The benefit is that we do have this additional information, so I agree that we should use it.