4 ms·

Anecdotally, I’ve found that codebases that enforce code coverage metrics often have worse behavior coverage than ones that don’t. It’s a classic example of Go

Anecdotally, I’ve found that codebases that enforce code coverage metrics often have worse behavior coverage than ones that don’t. It’s a classic example of Goodhart’s Law in action. Code coverage metrics only measure what percentage of code the test suite causes to run. But it’s very, very easy to write tests that run code without actually confirming that it produces correct output for all possible inputs. And it’s very, very easy to assume that a module with 90+% code coverage also has 90+% behavior coverage, and then become complacent about reviewing the suite for proper behavior coverage.

agentultra 20d ago
Djikstra seemed like he was mostly against testing. But only because he was for proofs. A unit test is a single example. The real way to demonstrate the absence of errors is to prove they aren’t there (vis a vis axioms and assumptions). But most developers don’t have the mathematical sophistication nor the time. It’s not that unit testing is useless. Just good to know what their limitations are and to plan your testing strategy accordingly.
- bunderbunder 20d ago
  You also have the problem of potentially having to re-verify everything by hand for every little change. Maybe fine for the kinds of projects Dijkstra was working on, but less practical in a business setting. Tools like QuickCheck and Hypothesis are an interesting middle ground, though. I strongly prefer them over standard-issue unit testing for verifying algorithm implementations.
  - agentultra 20d ago
    Hundred percent. All about trade-offs. Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios. TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.
    - bunderbunder 19d ago
      Yeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve that problem, but perhaps they can mitigate it.
      - agentultra 18d ago
        I think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.

agentultra 20d ago

Djikstra seemed like he was mostly against testing. But only because he was for proofs. A unit test is a single example. The real way to demonstrate the absence of errors is to prove they aren’t there (vis a vis axioms and assumptions). But most developers don’t have the mathematical sophistication nor the time. It’s not that unit testing is useless. Just good to know what their limitations are and to plan your testing strategy accordingly.

bunderbunder 20d ago
You also have the problem of potentially having to re-verify everything by hand for every little change. Maybe fine for the kinds of projects Dijkstra was working on, but less practical in a business setting. Tools like QuickCheck and Hypothesis are an interesting middle ground, though. I strongly prefer them over standard-issue unit testing for verifying algorithm implementations.
- agentultra 20d ago
  Hundred percent. All about trade-offs. Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios. TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.
  - bunderbunder 19d ago
    Yeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve that problem, but perhaps they can mitigate it.
    - agentultra 18d ago
      I think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.