>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.
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.