[marcosdumay]

You mean mutability annotations or allowing mutability at all?

Because you can't simply disallow mutability in an imperative language.

But about annotations, you annotate your code to let the compiler know what you meant to do. If just looking at what you do was enough, C would be a safe language. You improve it by giving more information to the compiler, so it can check if you are doing what you meant to.

(But I don't know what relation you saw with TCO. It's not a related concept.)