This might sound good to a TDD practitioner, but I'd suggest that the value of tests is that they independently verify an implementation. Couple them directly and soon you will be writing tests on your tests.

OTOH, saying "this must be true" and letting the compiler work it out sounds a lot like logic programming.

I've felt testing can be reduced to writing those functions twice and hoping at least one is correct. There has to be a better way.

The best way is making no mistakes :)

The second best is machine-checkable proofs, like types.

The fallback is tests. Sometimes the first two can't be applied.

BTW this is called "program synthesis" and there's a lot of research in the area right now. It only works for tiny programs at the moment.

Program Synthesis is Possible https://www.cs.cornell.edu/~asampson/blog/minisynth.html

ILP + IFP are easy to understand techniques of 'programming by example'.

Isn't that just a declarative language, or prolog?