The insight behind Knuth's glib "I have only proved the program correct" quote is that proofs can still contain our untested assumptions. It's possible for someone to carry over an untested and wrong assumption from the implementation to the proof without ever finding out it is incorrect.
Of course, the same is true for tests. If you prove the wrong thing, your code obviously won't be correct. If you test the wrong thing, your code obviously won't be correct.
However, if you prove the right thing, your code is correct. If you test the right thing, you code is correct in the cases you tested.
And yet, for whatever reason, only having tests is fine but only having proof isn't.
There's no way to prove that you proved the right thing, unfortunately. And, of course, your proof may not be correct. (Proof checkers can help, and I would have confidence in the correctness of a type-check as proof.)
Only having tests is "fine" for most circumstances because, unfortunately, proofs are intractable for most systems. During a software engineering talk I recently attended, an interview candidate stated that the largest proved-correct code base is on the order of 10,000 lines of code. Most people don't have the resources to do even that.
But, philosophically, I always want tests for the same reason that I run experiments: I want empirical evidence, not just reasoning. Empirical evidence increases my confidence that we have accounted for what we think we have.
