I appreciate that I am not the only one seeing the connection between property based testing and proofs.

I will quibble a little with their characterization of proofs as being more computationally impractical.

Proof verification is cheap. On a good day it is as cheap as type checking. Type checking being a kind of proof verification. That said writing proofs can be tricky.

I am still figuring out what writing proofs requires. Anything beyond what your type system can express currently requires a different set of tools (Rocq, Lean, etc) than writing asserts and ordinary programs. Plus writing proofs tends to have lots of mundane details that can be tedious to write.

So while I agree proofs seem impractical. I won't agree the reason is computational cost.

Recently asked Claude Code how to do more thorough tests and described how I imagine it and it set up Hypothesis and mutmut testing. The latter is quite cool, it introduces bugs in the code like swapping values and relational operators and checks if any test catches the bug. If not, your tests are probably not thorough enough. Better than just line coverage checks.

• aitchnyu

  today at 1:24 PM

  Is my intuition correct that Mutmut has far better ROI than Hypothesis? And its as necessary as code coverage?

  • whattheheckheck

    today at 1:47 PM

    In large code bases it is extraordinarily slow so you have to use it sparingly

Fuzzing as a concept is heavily underused in routine testing. People will usually focus on positive flows and some obvious/typical negative ones. But it's almost impossible to have the time to write exhaustive testing to cover all negative and boundary scenarios. But the good news is, you don't actually have to. There are so many tools now that can almost exhaustively generate tests for you at all levels. The bad news, they are not so widely used.

• esafak

  today at 2:06 PM

  What do you use?

  • ludovicianul

    today at 3:53 PM

    I'm using pitest for unit test mutations. And I've actually wrote a tool I'm using for REST API fuzzing. It's called CATS.

    • esafak

      today at 4:02 PM

      Presumably https://endava.github.io/cats/

Would you call it a K-top Defect Hunter?

• esafak

  today at 2:07 PM

  Not if the kids are within earshot, else I'll have to suffer those infernal songs again.

Using the phrase "without the benefit of hindsight" is interesting. The hardest thing with any technology is knowing when to spend the effort/money on applying it. The real question is: do you want to spend your innovation tokens on things like this? If so, how many? And where?

Not knocking this, just saying that it is easy to claim improvements if you know there are improvements to be had.

• esafak

  today at 3:13 PM

  That's what experience is for.