Warming Up to Unit Testing

Re:Warming Up to Unit Testing by bluGill on Tuesday February 25, 2020 @08:15AM (#22412893)

Formal methods don't beat unit tests for one important reason: it is much easier to reason about the single case the unit test covers and convince yourself it is correct than about all the possible cases (which might be an infinite set) at the same time. As Donald Knuth has said "Beware of bugs in the above code; I have only proved it correct, not tried it". Because even Knuth himself is smart enough to know he sometimes makes mistakes in his proofs. Just a few trials (ie unit tests) give confidence it works in practice and in theory.

Or to put it a different way, unit tests guard against an incorrect specification. Code can be proven correct and wrong at the same time. Unit tests make it much easier to reason about if what is specified to happen is what should happen.

As an aside, I'm not against blurring the line between unit tests and integration tests.

[ Parent | on HN ]

Re:Warming Up to Unit Testing by crimsonalucard on Tuesday February 25, 2020 @08:55AM (#22413170)

>Formal methods don't beat unit tests for one important reason: it is much easier to reason about the single case the unit test covers and convince yourself it is correct than about all the possible cases (which might be an infinite set) at the same time.

Dependent types and/or automated proof checkers should bridge the gap of intuitive reasoning. Basically the dual relationship where code verifies the type and dependent types verify the code should be strong enough to forego unit tests and guard against "incorrect specification."

>As an aside, I'm not against blurring the line between unit tests and integration tests.

Sure that's fine. But then the type of test and the context of what I am referring to is strictly tests that only cover pure mathematical logic.

Things outside of that bound cannot be covered by proof nor by programming methodology and are also not the type of test I am referring to.

[ Parent | on HN ]