Is there a language that has proper exclusively checked exceptions? That is, not just syntax sugar around checking an error value (à la Swift), but actual “the processor signals an exception” semantics, but all exceptions are still enforced to be handled-or-passed by the compiler?

Honest question, because I can’t think of any. I can see it being advantageous to have checked-only exceptions but there has to be a good reason why it’s so rare-to-never that we see it.

I’m not sure how else you’d get the holy grail, which I’d define as:

1. The compiler enforces that you either handle an exception or pass it to the caller

2. Accurate and fine-grained stack traces on an error (built-in, not opt-in from some error library du jour)

3. (ideally) no runtime cost for non-exception paths (no branches checking for errors, exceptions are real hardware traps)

C++ has 2 and 3, Java has only 2 (because RuntimeException exists), Rust has only 1. I’d love a language with 1 and 2, but all 3 would be great.

I can't think of any either. A sibling commenter suggests maybe Eiffel but I haven't really tried or looked at that language so I don't know if it's true. I think having all 3 would be great but if I can only choose one of them I personally prefer #1.

I've heard Eiffel has them better, but haven't used it.

And then Koka too, but I have zero experience...

Someon might shine light here about this...