Another way to think like this is to approach testing using fuzzing, but in a way that is designed to have 100% coverage of invariants.
Basic fuzzing generates random inputs looking for a crash, without asserting invariants along the way. Invariant fuzzing, on the other hand, is concerned not just with the inputs to a function but also the outputs.
For example, if a function is expected to throw exceptions for bad inputs, then use invariant fuzzing to test that all exceptions are thrown for a variety of bad inputs. Writing an invariant fuzz test like this often takes less code than writing hundreds of unit tests, which have significantly less coverage.
Another example, and this is how we found CVE 2019-1543 in OpenSSL [1]. For all the AEAD ciphers in OpenSSL that we wanted to support, we fuzzed [2] and round-tripped various combinations of {key, iv, plaintext/ciphertext, aad, tag}, comparing against an independent interface, while also randomly corrupting bytes in {key, iv, ciphertext, aad, tag} to ensure that AEAD authenticity invariants were being kept by OpenSSL. We needed the "A"s in the AEADs so we tested them.
Adding this AEAD authenticity invariant test to our fuzz test took 25 lines of code and found the CVE in literally a second.
After the CVE was found, OpenSSL added a test vector. This was 8 lines of code, and tested authenticity only for a single test vector, without covering the entire range of IV lengths, which was the root of the issue that the CVE uncovered. All this effort, for little gain, when the whole spectrum could have been tested across a few thousand vectors in the same amount of code.
If you are interested in this kind of thing, Guido Vranken is taking the same approach to the next level for multiple crypto libraries [3].
F* is rad! Idris indeed still has some way to go to be production ready but I like to give it relevant attention when I can. It's like a reimagined Haskell :)
Another way to think like this is to approach testing using fuzzing, but in a way that is designed to have 100% coverage of invariants.
Basic fuzzing generates random inputs looking for a crash, without asserting invariants along the way. Invariant fuzzing, on the other hand, is concerned not just with the inputs to a function but also the outputs.
For example, if a function is expected to throw exceptions for bad inputs, then use invariant fuzzing to test that all exceptions are thrown for a variety of bad inputs. Writing an invariant fuzz test like this often takes less code than writing hundreds of unit tests, which have significantly less coverage.
Another example, and this is how we found CVE 2019-1543 in OpenSSL [1]. For all the AEAD ciphers in OpenSSL that we wanted to support, we fuzzed [2] and round-tripped various combinations of {key, iv, plaintext/ciphertext, aad, tag}, comparing against an independent interface, while also randomly corrupting bytes in {key, iv, ciphertext, aad, tag} to ensure that AEAD authenticity invariants were being kept by OpenSSL. We needed the "A"s in the AEADs so we tested them.
Adding this AEAD authenticity invariant test to our fuzz test took 25 lines of code and found the CVE in literally a second.
After the CVE was found, OpenSSL added a test vector. This was 8 lines of code, and tested authenticity only for a single test vector, without covering the entire range of IV lengths, which was the root of the issue that the CVE uncovered. All this effort, for little gain, when the whole spectrum could have been tested across a few thousand vectors in the same amount of code.
If you are interested in this kind of thing, Guido Vranken is taking the same approach to the next level for multiple crypto libraries [3].
[1]: https://nvd.nist.gov/vuln/detail/CVE-2019-1543
[2]: https://github.com/ronomon/crypto-async#tests
[3]: https://github.com/guidovranken/cryptofuzz