“The difference is that with Hypothesis you test properties empirically, where with Coq you formally prove them. “
One can also do property/spec-based testing in proof assistants. So, you can get empirical and formal assurance in Coq. One implementation is QuickChick.
“Property testing, on the other hand, can help you identify edge cases you would not have otherwise anticipated. “
I usually think of random testing doing that with PBT confirming or rejecting conformance to a user-supplied spec. Thinking on the author’s comment, it is possible that the random input that PBT generates might break the software in a different way than your specs intended. So, author is right. I’ll have to tie that in to future recommendations. I still theorize that random testing is still best at this, though.
“Property testing also provides a framework that makes refactoring easy.”
Design by contract should be considered for that. Property-based testing is almost there since the properties are like the contracts. It just doesn’t put them in as optional runtime checks. That can be valuable for catching refactoring or integration problems in development and production. Best route I’ve seen combines such contracts with PBT based on them and random testing using them to find specific points of failure.
Nice writeup. A few things I noticed.
“The difference is that with Hypothesis you test properties empirically, where with Coq you formally prove them. “
One can also do property/spec-based testing in proof assistants. So, you can get empirical and formal assurance in Coq. One implementation is QuickChick.
“Property testing, on the other hand, can help you identify edge cases you would not have otherwise anticipated. “
I usually think of random testing doing that with PBT confirming or rejecting conformance to a user-supplied spec. Thinking on the author’s comment, it is possible that the random input that PBT generates might break the software in a different way than your specs intended. So, author is right. I’ll have to tie that in to future recommendations. I still theorize that random testing is still best at this, though.
“Property testing also provides a framework that makes refactoring easy.”
Design by contract should be considered for that. Property-based testing is almost there since the properties are like the contracts. It just doesn’t put them in as optional runtime checks. That can be valuable for catching refactoring or integration problems in development and production. Best route I’ve seen combines such contracts with PBT based on them and random testing using them to find specific points of failure.