> obvious for someone who programs primarily in imperative languages, like top-down, line by line execution in functions or local variables in functions.

This makes me angry at "ordinary" programmers. They think it's obvious, but they never rigorously modelled the sequential execution in the first place. Instead, they use their instinct. Instinct is efficient, but when it's wrong, tough luck.

This is probably why proving the correctness of a program is so difficult: you have to pin everything down mathematically, including sequences of side effects. For most people, that's much more difficult than merely relying on their guts. As a result, no one proves their programs. Maybe they test them.

With Haskell, you can't even program without pinning it all down mathematically. As a result, no one uses Haskell… OK, not no one, but still that's a significant barrier to entry.

I wish programmers were more mathematically aware. I wish they realised they're doing applied math, whether they like "math" or not. I'm tempted to blame our education, but I'm not sure it's the only culprit.