When discussing well typed-ness, and with more complex languages where you have weird undecideable components, you can end up with a notion of "Well typed" as f

When discussing well typed-ness, and with more complex languages where you have weird undecideable components, you can end up with a notion of "Well typed" as follows: e: T is well typed _if_ the end result of e would be of type T (end result being hand-wave-y) It's not a guarantee that e is a value of a certain type, but a guarantee that if e is a value in the first place, then it will be a certain type. You sidestep having to prove the halting nature of e. This leaves a nice spot for computation that doesn't complete! let y = return 1 f(y) y could be any type, and it's well typed, because you're never in a secnario where f(y) will be provided a value of the wrong type. Well-typed-ness, by my understanding in more complex type system, is not a guarantee of control flow, but a guarantee that _if_ we evaluate some expression, then it will be fine. And so... you can put `!` as a type in your system, treat return as an expression, and have a simpler semantic model, without really losing anything. Less moving parts, etc.... that's my read of it anyways.