I might have been convinced if mathematical proofs were not expressed in code. If a proof can exhaustively cover the problem space, then there's no need for further testing.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Static analysis is an incredibly useful tool, not denying it. I am saying we should avoid worshipping at its altar. Any useful program is incredibly complicated and needs some kind of run time testing.
When I wrote Ruby/Javascript, I remember needing to write unit tests that verified types of input/output variables. These kinda tests were undifferentiated boilerplate that needed to exist but didn't need to be written by me. Especially since there were many tests I'd forget to add or would intentionally not add because the test file was getting obnoxiously large.
Factoring out those boilerplate tests into the compiler (when using Java, Rust, or TypeScript) was very valuable to me, but didn't change the fact that they are basically automatically generated unit tests. The borrow checker in Rust is a similar factoring out of automatically generated unit tests, which I wouldn't have typically written.
Continuing to push more undifferentiated unit testing into the compiler/libs/proofs helps make sure I only need to write domain specific unit tests.
Why do you feel static analysis and compile time unit testing are different? or do you mean, domain agnostic testing is ok, but really we need domain specific testing?
When I write in dynamically typed language I never write tests like that. I'm more familiar with static than dynamic, but are experts really doing that kind of thing?
That'd be a case for design by contract.
Jokes aside, if my problem is small enough to be proved (for whatever value of small), I do not see any more value to be extracted from tests. Who bothers checking that 3+2 = 2+3 after proving that x+y = y+x?
But yes, formal methods make testing a lot easier and taken far enough, can suffice on their own.
I think that comes under "taken far enough". If you can model the corruption in your proof, you're good. I'm less confident about timings. But you're right that testing is still useful for bugs on other levels. After all, going high enough, humans can have buggy requirements, and no proof will catch that. Tests might.