fair enough. I was thinking more on the side of "this rewrite should be correct and indeed it is" by asking the tool to come up with a proof rather than doing extensive testing.
Cosette can prove equivalency but not correctness. Unit testing can't prove correctness either but it can demonstrate that specific conditions are satisfied.
If you have a query 1 that satisfies case a and b but then identify a bug and add case c you can write a query 2 which satisfies a, b and c and indeed Cosette may identify that case as the difference (or not!) but you still have no guarantee that you will not then discover case d which is not satisfied by 1 or 2 or a future 3.
Even if the two queries are provably equivalent, that does not mean that the database engine will produce the same results for the two. There could be bugs in the implementation.
