(rant incoming)
This is actually something that bothers me with contemporary programming languages - the huge amount of implicit state due to function calls on the stack and the way the heap is organized. I'm much more in favor of a data-oriented design where you don't get to freely allocate objects, but need to strictly organize them according to a model. I imagine this would also make formal verification a lot easier, since you have a single global coherent view of the program state, kind of like being forced to store all important program state in a database (except more efficient since it's just memory).
Ironically I've become a big fan of global variables. In my experience the classic criticism of "anything could modify anything" doesn't really hold - using globals enables me to statically analyze all usages, not to mention setting memory breakpoints becomes much easier as well - I always know what I want to watch, instead of it being some pointer that will be allocated at some unknown time, 20 stack frames away from the actual usage.