9 ms·

That very much depends on the type system you use. With (for example) refinement types and dependent types you can prove your code correct with zero tests neede

That very much depends on the type system you use. With (for example) refinement types and dependent types you can prove your code correct with zero tests needed. Examples are F*, Idris, Agda, Coq etc.

techdragon 4y ago
Prove the code is correct per the design, it doesn’t eliminate the possibility of design errors which can still benefit from tests (or QuickCheck like tools) to ensure that what you design does what you think it does … a critical component given how rarely you see these languages used to actually build large applications in the wild.
- deterministic 4y ago
  The key difference is that with proven correct code you actually have a formal spec you can prove properties about. Without proven correct code you don’t even have a formal spec. Just a bunch of random tests (if you are lucky) that may or may not match your informal spec. And the argument that if you can’t prove your design correct then there is no point proving your code correct is a strange one. That’s like saying that there is no point writing tests because you can’t prove your design correct or guarantee that all tests needed will be written. Ehhhh nope. I have written and generated more than 9000 tests for a very large scale C++ applications that are used by large corporations around the world. And I haven’t had a bug in production for 5+ years. However I of course can’t prove that those tests cover everything or that my design is correct. But that doesn’t mean it isn’t worth doing.
  - pdimitar 4y ago
    Yeah, I feel way too many people mistake "we can't cover 100% of everything" with "it's not worth tightening the bolts". Strange conflation but a very common one indeed.
astrange 4y ago
All well-formed code is always a correct version of itself (Curry-Howard correspondence). It's just that sometimes you thought it was a correct version of something else and turn out to be wrong about that. Since dependent type systems are just another kind of code, this is still true.

techdragon 4y ago

Prove the code is correct per the design, it doesn’t eliminate the possibility of design errors which can still benefit from tests (or QuickCheck like tools) to ensure that what you design does what you think it does … a critical component given how rarely you see these languages used to actually build large applications in the wild.

deterministic 4y ago
The key difference is that with proven correct code you actually have a formal spec you can prove properties about. Without proven correct code you don’t even have a formal spec. Just a bunch of random tests (if you are lucky) that may or may not match your informal spec. And the argument that if you can’t prove your design correct then there is no point proving your code correct is a strange one. That’s like saying that there is no point writing tests because you can’t prove your design correct or guarantee that all tests needed will be written. Ehhhh nope. I have written and generated more than 9000 tests for a very large scale C++ applications that are used by large corporations around the world. And I haven’t had a bug in production for 5+ years. However I of course can’t prove that those tests cover everything or that my design is correct. But that doesn’t mean it isn’t worth doing.
- pdimitar 4y ago
  Yeah, I feel way too many people mistake "we can't cover 100% of everything" with "it's not worth tightening the bolts". Strange conflation but a very common one indeed.

astrange 4y ago

All well-formed code is always a correct version of itself (Curry-Howard correspondence). It's just that sometimes you thought it was a correct version of something else and turn out to be wrong about that. Since dependent type systems are just another kind of code, this is still true.