undefined | Better HN

0 pointsagentultra2y ago0 comments

I meant "prove" as in, "mathematically proven." That is, for all possible inputs your theorem holds. A unit test is only an example of one such input. They don't prove there are no bad inputs.

There are many places in programming where you don't care to prove properties of your program to this level of rigor; that's fine -- sufficiency is an important distinction: if a handful of examples are enough to convince you that your implementation is correct with regards to your specifications, then it's good enough. Does the file get copied to the right place? Cool.

However there are many more places where unit tests aren't sufficient. You can't express properties like, "this program can share memory and never allows information to escape to other threads." Or, with <= 10 writers all transactions will always complete. A unit test can demonstrate an example of one such case at a time... but you will never prove things one example at a time.

0 comments

2 comments · 1 top-level

pfdietz2y ago· 1 in thread

Well that's silly. You're not arguing against unit tests, you're arguing against testing in general. But empirically testing does improve the reliability of software. You're tossing the baby out with the bathwater in the interest of an academic ideal of proved correctness.

I will add that if you are verifying the correctness of some code, you have a formal specification of what the code is supposed to do. That is, you have a description of valid inputs, and a formula determining if the output is correct, given those inputs. But if you have those, you can also do property-based testing: generate random inputs that satisfy the input properties, and check that the output satisfies the output condition. This is all easier that proving correctness (it requires little or no manual intervention) and gives much of the same benefit.

agentultraOP2y ago

Maybe you need to re-read my original comment. I’m arguing for sufficient evidence of correctness. Unit tests often provide that for a good deal of software. I think people ought to write more of them.

However I think folks do get dogmatic about testing and will claim things like, “all you need is unit/integration/types.”