DbC moves the specification of what a function should do out of doc-strings and test cases and into machine readable code! With fuzzing today, you send one str

DbC moves the specification of what a function should do out of doc-strings and test cases and into machine readable code! With fuzzing today, you send one stream of input into an entire program, hope for a crash, then figure out where in the entire execution of the program up to that point things went wrong. You have to figure out how to generate inputs that will exercise every pathway. However, if you had pre and postconditions for every function, you could automatically fuzz individual functions! You don't have to wait for 99% of inputs to get rejected because they don't have the right header. The "unit-fuzzer" would only generate valid inputs for the function it is testing, and check that the function produces valid output, as well as valid inputs for the functions it calls. If you have n functions of complexity k, fuzzing or verifying an entire program takes time k^n. However, if you have pre/postconditions, you can verify every function with k*n work. If you have enough cores, you can do this in parallel in k time. That's insane.