Earlier quoted context omitted.
> they prove nothing If they fail, they prove there's a bug (in either the test or the code.) This is like literally any other kind of test.
I meant "prove" as in, "mathematically proven." That is, for all possible inputs your theorem holds. A unit test is only an example of one such input. They don't prove there are no bad inputs. There are many places in programming where you don't care to prove properties of your program to this level of rigor; that's fine -- sufficiency is an important distinction: if a handful of examples are enough to convince you t…
I will add that if you are verifying the correctness of some code, you have a formal specification of what the code is supposed to do. That is, you have a description of valid inputs, and a formula determining if the output is correct, given those inputs. But if you have those, you can also do property-based testing: generate random inputs that satisfy the input properties, and check that the output satisfies the output condition. This is all easier that proving correctness (it requires little or no manual intervention) and gives much of the same benefit.