The problem is strongly tied to whether exceptions are checked if you want to have the type system support you in checking and validating your reasoning about the contracts between callers and callees. With unchecked exceptions, unless you have extreme discipline and document exception types for every function, and take care to use dedicated exception types for all non-bug exceptions, effectively emulating what the type-checker does for you with checked exceptions; unless you do all that, it's a fool's errand in terms of ensuring (being able to prove the correctness of) your interface contracts.