That was the basic premise of checked exceptions in Java. It's not really related to the type system or anything. The root of the problem is Java compiles each

That was the basic premise of checked exceptions in Java. It's not really related to the type system or anything. The root of the problem is Java compiles each class as an independent module, so any method has to deal with all its exceptions, even if only naming them, or it can't compile. Thus checked exceptions meant you either got huge signatures, or you wound up wrapping them all into other exceptions, which then made them much harder to inspect. And unchecked exceptions made the problem worse. Java uses single-inheritance and put unchecked exceptions on their own branch. This meant you wound up with, for example, IOException and UncheckedIOException with no close common ancestor, so you had to wrap one in the other. So now, in addition to complicated signatures, you are doing more wrapping. I think what might work would be to ditch the checked / unchecked idea, mostly. (You still want to treat errors like division by zero or invalid array indexing as unchecked.) What you distinguish instead is whether methods are "safe" or "unsafe". An unsafe method can still catch some exceptions, it just doesn't promise to catch all of them. The safe method must catch everything. For example, your main method and Thread.run would have to be safe.