I would love something like this where to write a function with side effects I'd have to annotate it as such.

Then the compiler could recursively understand whether any given function is pure.