A good set of unit tests partitions the input space into parts, and then provides an existence proof that the program is correct for an example chosen from each part.
A good formal proof does the same, but provides a universal proof that the program is correct for all examples chosen from each part.
Both strategies can fail if they miss an important part of the input set. Unit tests can also fail if a program is “adversarial” and fails in a specific input that isn’t the particular example.
In practice, achieving “a good set of unit tests” requires you to mentally work out how to partition the input set in a way that matches your program, and at that point you’re most of the way to proving it correct, so you might as well do that. It still might make sense to write unit tests if you don’t have the tooling to enforce a mechanical proof.
A good set of unit tests partitions the input space into parts, and then provides an existence proof that the program is correct for an example chosen from each part.
A good formal proof does the same, but provides a universal proof that the program is correct for all examples chosen from each part.
Both strategies can fail if they miss an important part of the input set. Unit tests can also fail if a program is “adversarial” and fails in a specific input that isn’t the particular example.
In practice, achieving “a good set of unit tests” requires you to mentally work out how to partition the input set in a way that matches your program, and at that point you’re most of the way to proving it correct, so you might as well do that. It still might make sense to write unit tests if you don’t have the tooling to enforce a mechanical proof.