> I don't see any fundamental reason why such functionality couldn't be brought into an imperative language at some point (but maybe I'm ignorant about PL theor

> I don't see any fundamental reason why such functionality couldn't be brought into an imperative language at some point (but maybe I'm ignorant about PL theory). Nim can kinda do this with its effect tracking feature (although I haven't used Nim enough yet to know if anyone is really using it), e.g. type AEffect = object of RootEffect BEffect = object of RootEffect proc callA() {.tags: [AEffect].} = echo "A" proc callB() {.tags: [BEffect].} = echo "B" proc somethingInBetween() = # Tags are inferred here. callA() proc doSomethingWithA() {.tags: [AEffect].} = somethingInBetween() # trying to `callB()` here would fail. proc doSomethingWithB() {.tags: [BEffect].} = callB() # trying to `callA()` here would fail. The `tags` pragma adds specific tags to the proc and the compiler ensures that it doesn't call anything with any other tags. Similar mechanism is used for exceptions too.