One thing to remember when using an assertion-based method is what it can be used for:
1. Unambiguous specifications [vs human language] of exactly what the function expects, should maintain, and should output. This is basis of Design-by-Contract method of verification in Eiffel (original), Ada, and SPARK.
2. Ability to check inconsistencies on that if a formal, specification tool. An example is where unique types are defined for miles and kilometers that require a conversion before used in same-sized variable. Might have prevented a rocket from being destroyed.
3. Ability to formally prove through automated or interactive means that your code has those properties in all cases rather than whatever you tested for or your fuzzer came up with. Frama-C, Java w/ JML, and SPARK Ada can do this with SPARK the champ so far. It's hard and limits how you express the problem or what problems it can handle but with highest payoff in correctness. Anything unproven can be handled by a runtime check the tool might even insert for you.
4. Academic and commercial tools exist that can automatically generate tests from those specs. So, you get tests covering whatever you can specify automatically with no human effort. You can use your brain on stuff the tools can't handle.
5. Ability to do equivalence checks more easily on annotated (i.e. constrained) programs can help show optimizations or compilations didn't break your program.
6. The annotations might also be used for synthesizing programs or optimizing them even more than usual.
So, these are some benefits that come from leaning toward formal specs of code or within code instead of just manual, unit testing.
I'm a big fan of design by contract - at least how it's implement in racket (blame at module boundaries and higher order contracts). I wonder how quickcheck type testing slots into the picture.
1. Unambiguous specifications [vs human language] of exactly what the function expects, should maintain, and should output. This is basis of Design-by-Contract method of verification in Eiffel (original), Ada, and SPARK.
2. Ability to check inconsistencies on that if a formal, specification tool. An example is where unique types are defined for miles and kilometers that require a conversion before used in same-sized variable. Might have prevented a rocket from being destroyed.
3. Ability to formally prove through automated or interactive means that your code has those properties in all cases rather than whatever you tested for or your fuzzer came up with. Frama-C, Java w/ JML, and SPARK Ada can do this with SPARK the champ so far. It's hard and limits how you express the problem or what problems it can handle but with highest payoff in correctness. Anything unproven can be handled by a runtime check the tool might even insert for you.
4. Academic and commercial tools exist that can automatically generate tests from those specs. So, you get tests covering whatever you can specify automatically with no human effort. You can use your brain on stuff the tools can't handle.
5. Ability to do equivalence checks more easily on annotated (i.e. constrained) programs can help show optimizations or compilations didn't break your program.
6. The annotations might also be used for synthesizing programs or optimizing them even more than usual.
So, these are some benefits that come from leaning toward formal specs of code or within code instead of just manual, unit testing.