3 ms·

I wish static analysis were always sufficient. Curry-howard doesn't obviate the need for tests. Anything affected by the physical implementation of the computer

I wish static analysis were always sufficient. Curry-howard doesn't obviate the need for tests. Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases, timing side channels in cryptography, all high-integrity code, and so on. Proofs can also be buggy themselves, as can the verifiers. But yes, formal methods make testing a lot easier and taken far enough, can suffice on their own.

rhn_mk1 5y ago
> Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases 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.