They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs s

They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks. I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode. I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.