The primary benefit imo is * Way of thinking and discipline. Instead of adhock assertions, you deliberately state in code "These are the preconditions, invaria

The primary benefit imo is * Way of thinking and discipline. Instead of adhock assertions, you deliberately state in code "These are the preconditions, invariants, and postconditions" of this function/module * Better error messages. * Better documentation (can automate extracting the contracts as documentation). * Better tooling. Can automate creating tests from preconditions. You can sample the functions input space and make sure invariants and postconditions hold. It's like, do you name all your functions 'func a1, func a2, func a3' or do you provide better names?