"I keep hearing that it’s easier to analyze pure functional code than mutable imperative code. But nobody gives rigorous arguments for this and nobody provides

"I keep hearing that it’s easier to analyze pure functional code than mutable imperative code. But nobody gives rigorous arguments for this and nobody provides concrete examples." I believe the first sentence and here is my personal justification for it (maybe it can be made into rigorous argument). I base this on my experience with Haskell, and it might be that typing and control of side effects is actually essential for the claim. In Haskell, for the most part, results of a function depend solely on its arguments. So you can treat the inner workings of function as a black box, and only worry about the "boundary" of type information of its parameters. Now imagine you're facing a large program and you want to estimate an effort required to make a change. In functional programs, if you look at a function, you can see the scope of what the function does from its type (its parameters). In imperative programming, a function can do anything to the system under the hood, there are no natural boundaries. It's very similar to the real world, where you can estimate for example effort in building something, like renovating an appartment, solely based on the size of the object. You know immediately that renovating a small appartment is (most likely) less effort than building a skyscraper, because of its size. In imperative programming, we're often faced with TARDIS-type deals - bigger on the inside than on the outside. In physics, there is divergence theorem that formalizes this notion of "you don't have to look inside the object, you can only look at what happens at the boundary". Similarly, functional programming (when done right) creates the boundary at the function level, so you can then apply this type of reasoning to it. "I chose correctness because it was the easiest to objectively verify. I’m sure that if I posed a similar challenge about refactoring code, everybody would be telling me that “being easier to reason” isn’t about refactoring, it’s clearly about correctness!" I am not sure he is right there. The setting up of the boundaries in functional programs is real. Yet, with current type systems, the boundaries are not watertight. And of course, you can always write your program in imperative style with functional programming language, without an effective boundary. I think the OP ignores the boundary setting question, because if you want a full proof of something, then you don't need to have the boundaries. But that's what ultimately helps in understanding. Maybe if he tried to prove several different statements about the code, then the boundaries would help, because he could reuse the theorems about things delineated at the boundary. I think working with FP correctly essentially forces you to prove statements about the code (for example, this function doesn't have side effects), and then you can reuse these small statements for formally proving something else about it. Whereas in IP, you don't build these statements, you have to build them for the formal proof explicitly. The resulting proofs, written down, will have the same lengths, but in the FP case some work might have already been done. So what OP is saying is similar to say, well, divergence theorem is really useless, because at the end of the day, you have to correctly account for all your sources and sinks. Which is true in a way, but it is a useful theorem nonetheless.