3 ms·

> no static analysis on earth is going to stop you from actually needing tests to see if your code works. I might have been convinced if mathematical proofs we

> no static analysis on earth is going to stop you from actually needing tests to see if your code works. 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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

LAC-Tech 4y ago
Fair point, but would you deploy un-tested code to production based on a static proof? AFAIK the issue with this stuff is that the kinds of problems proofs are able to practically cover are very small. 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.
- yazaddaruvala 4y ago
  I don't feel like static analysis and unit testing are very different things. Given that my unit tests run roughly at compile time (ideally they would run during compile), it really isn't different than static analysis. Especially unit tests where all the inputs are mocked and expected outputs are provided. 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?
  - LAC-Tech 4y ago
    When I wrote Ruby/Javascript, I remember needing to write unit tests that verified types of input/output variables. 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.
- rhn_mk1 4y ago
  Sure, sometimes I even deploy code without a proof nor tests ;) 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?
emerged 4y ago
I took computer language theory in college literally 20 years ago, had a sandwich with chips during every class. I clicked on that link and could taste the sandwich.
AlotOfReading 4y ago
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 4y 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.

LAC-Tech 4y ago

Fair point, but would you deploy un-tested code to production based on a static proof? AFAIK the issue with this stuff is that the kinds of problems proofs are able to practically cover are very small. 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.

yazaddaruvala 4y ago
I don't feel like static analysis and unit testing are very different things. Given that my unit tests run roughly at compile time (ideally they would run during compile), it really isn't different than static analysis. Especially unit tests where all the inputs are mocked and expected outputs are provided. 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?
- LAC-Tech 4y ago
  When I wrote Ruby/Javascript, I remember needing to write unit tests that verified types of input/output variables. 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.
rhn_mk1 4y ago
Sure, sometimes I even deploy code without a proof nor tests ;) 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?

emerged 4y ago

I took computer language theory in college literally 20 years ago, had a sandwich with chips during every class. I clicked on that link and could taste the sandwich.

AlotOfReading 4y ago

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 4y 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.