3 ms·

Unit tests operate in the same domain and constraints as formal methods. In terms of correctness formal methods beat unit tests hands down. For things that liv

Unit tests operate in the same domain and constraints as formal methods. In terms of correctness formal methods beat unit tests hands down. For things that live outside of this domain the term integration test becomes relevant. If you are testing for unknown side effects it is no longer a unit test but an integration test. This is not my point. Unfortunately I can't go into detail about my point because it's just too long to talk about. I glossed over it and called it "Programming methodology." In the context of correctness, with the right programming methodology, programming language and type checker you can use this and your intuition alone to forego the need for unit tests. This does not apply to integration tests. Anyway without going in to deep the right programming methodology involves reducing complexity. It's similar to how if a programming doesn't have nulls you can't have runtime errors caused my nulls. If you use the right programming language or right methodology you can reduce much of the complexity of the program to the point where unit tests are redundant to your intuition. Another good example of a language that pulls this off is Rust or Haskell. You don't have to go as far as COQ but the previous two languages force you into a methodology that ensures correctness to a degree that many unit tests become redundant.

bluGill 7y ago
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.
- crimsonalucard 7y ago
  >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.

bluGill 7y ago

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.

crimsonalucard 7y ago
>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.