Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and cl

Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the unfamiliar think of a more principled version of GOTO), so in a real sense intuitionistic proofs are more direct. The double-negation translation then corresponds to implementing continuations in a pure language using continuation-passing style. This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!