GlobalVsLocalReasoning

One concept that comes up in programming is that of "global" versus "local" reasoning. I haven't found another term to describe this.

When we study a piece of code, it will require "local" reasoning when we can understand its implementation without having to know the wider context of the program. Global reasoning on the other hand requires us to hop through files, figure out environment variables, and understand its use of global or thread-local variables. We also need to figure out its call-sites in order to understand how the function interacts with the wider system.

Here's an example:

thread_local! {
    pub static X: i32 = const { 0 };
}

fn f() {
    let x = MY_THREAD_LOCAL.with(|x| *x);
    // ...
}

Here we have to know how "MY_THREAD_LOCAL" is being manipulated before the function is called. "f" is a function that requires global reasoning. On the other hand, if this were a formal parameter, then it would require local reasoning.

Global reasoning is not desired

Global reasoning makes a program harder to reason about. Functions that require global reasoning complicate understanding that function. It's why programming in general settled on lexical scope instead of dynamic scope. Dynamic scope invokes global reasoning by default, whereas lexical scoping does not.

Local reasoning has some downsides. Consider how practical shell languages can be with their environment variables: MYENV=123 run-script. We don't need to deal with passing this input "MYENV" through all the various scripts to reach the receivin script. We avoid TrampData.

Unfortunately, I think we just have to accept - in general - that we should strive for local reasoning where feasible, even if it is more verbose and labor intensive. Sure, some cases demand global reasoning, but we ought to keep these to a minimum in order to prevent difficult to understand code.

Exceptions to the rule

When a function uses non-local (non-parameter) inputs, it can be locally reasoned about if it does not act as a leaky abstraction. Say we have an environment variable that is read by a function that informs it about whether to use SIMD instructions. If the function outputs the same information regardless of this variable being true or false, then it can be reasoned about locally.