3 ms·

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

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 5y 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 5y 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 5y 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?

yazaddaruvala 5y 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 5y 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 5y 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?