Crosscut

Checked exceptions require annotations in a function's signature. A function is not allowed to throw a checked exception, unless that specific exception is noted there. If the function calls other functions that could throw exceptions, it must add those exceptions to its own signature, or handle them internally.

If the compiler infers all that (and I see no reason why it couldn't), then this requires zero work from the developer, unless they decide to actually handle an error. (And remember: With a code database, inference can also be explicit, so nothing is hidden.)

There's a problem with exceptions though: They don't interact well with linear types, for the same reasons that algebraic effects don't. I was going to disregard exceptions as an option due to that. Now I'm no longer sure. But let's continue that line of thought on another day.