Hacker News Reader

Comment by odyssey7 | Hacker News Reader

This is a good idea, though I don’t think it would guarantee program equivalence beyond the test cases.

Depends on how comprehensive the test suite is.

And OK it's not equivalent to a formal proof, but passing 1,000+ tests that cover every aspect of the specification is pretty close from a practical perspective, especially for a visual formatting tool.

With mutation testing you can guarantee that all the behavior in the code is tested.

UC Berkeley: “Top-level functional equivalence requires that, for any possible set of inputs x, the two pieces of code produce the same output. … testing, or input-output (I/O) equivalence, is the default correctness metric used by the community. … It is infeasible to guarantee full top-level functional equivalence (i.e., equivalence for any value of x) with testing since this would require testing on a number of inputs so large as to be practically infinite.”

https://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-...

In practice mutation fuzz testers are able to whitebox see where branches are in the underlying code, with a differential fuzz test under that approach its generally able to fuzz over test cases that go over all branches.

So I think under some computer science theory case for arbitrary functions its not possible, but for the actual shape of behavior in question from this library I think its realistic that a decent corpus of 'real' examples and then differential fuzzing would give you more confidence that anyone has in nearly any program's correctness here on real Earth.

Yes, there are different levels of sureness being described.

When I hear guarantee, it makes me think of correctness proofs.

Confidence is more of a practical notion for how much you trust the system for a given use case. Testing can definitely provide confidence in this scenario.

How is that relevant for mutation testing?

You can guarantee that all the cases in the code are tested. That doesn't necessarily mean that all the behaviour is tested. If two implementations use very different approaches, which happen to have different behaviour on the Mersenne primes (for deep mathematical reasons), but one of them special-cases byte values using a lookup table generated from the other, you wouldn't expect mutation testing to catch the discrepancy. Each implementation is still the local optimum as far as passing tests is concerned, and the mutation test harness wouldn't know that "disable the small integer cache" is the kind of mutation that shouldn't affect whether tests pass.

There are only 8 32-bit Mersenne primes, 4 of which are byte-valued. Fuzzing might catch the bug, if it happened to hit one of the four other 32-bit Mersenne primes (which, in many fuzzers, is more likely than a uniform distribution would suggest), but I'm sure you can imagine situations where it wouldn't.

> but one of them special-cases byte values using a lookup table generated from the other, you wouldn't expect mutation testing to catch the discrepancy

Sure you would. If the mutation tester mutates that lookup table. Which is quite easy to do, and which mutmut will do (if that lookup table is inside a function, because mutmut is based on mutant schemata).

If the mutation tester mutates that lookup table, then that will eventually lead to all entries in the lookup table being tested. That does not mean that the four divergent values outside the lookup table will end up being tested.

I think if you hit full path coverage in each of them independently and run all the cases through both and check they're consistent you're still done.

Or branch coverage for the lesser version, the idea is still to generate interesting cases based on each implementation, not based solely on one of them.

If the buggy implementation relies indirectly on the assumption that 2^n - 1 is composite, by performing a calculation that's only valid for composite values on a prime value, there won't be a separate path for the failing case. If the Mersenne numbers don't affect flow control in a special way in either implementation, there's no reason for the path coverage heuristic to produce a case that distinguishes the implementations.

Well yeah, but then any discrepancies that are found can be discussed (to decide which of the behaviors is the expected one) and then added as a test for all existing and future implementations.

Reply on news.ycombinator.com