Seemingly the confusion is due to the multiple meanings of the word "return" here? One can visualize the annotation as [[aborts]] or [[terminates]], rather than

Seemingly the confusion is due to the multiple meanings of the word "return" here? One can visualize the annotation as [[aborts]] or [[terminates]], rather than "doesn't return". This is also why there's very little point to introspecting the presence of this annotation or even overloading based on this annotation. Discussing whether a function which always terminates "returns" or "not-returns" an int is as useful as discussing whether a function which is never executed returns an int. The semantic analysis is rather clear in both cases.