In trying to convince others that *global mutable state* is a bad idea, I realize I don't have any hard evidence - just abstract reasons. At the very least, I'd like an illustrative code example I could point to. Any suggestions?
Conversation
There's certainly literature that programmers struggle with aliasing + state. You don't even need *global* mutable state for that — just any mutable state that has aliases will do.
2
3
Neelakantan Krishnaswami talks more about this here: semantic-domain.blogspot.com/2018/04/are-fu
Basically aliasing + mutability + procedures are the unholy triad, and program analysis becomes a lot easier when you have only two
1
1
9
While I enjoyed reading the blog post, to my mind it's a great example of the very opposite of what the OP asked for, which is "hard evidence" as opposed to "abstract reasons". (Well, YMMV, but it's still pretty much shaded over to the latter side.)
1
1
I might be coming at this from an FM perspective, but the fact we need new logics to handle it indicates it's harder to verify. Though that does not automatically mean it's harder to use from an engineering perspective.
1
3
I often use a rule of thumb that 'being harder to verify', often overlaps with 'being hard for humans to understand'. It'd be nice to have some harder data on this. A counterexample could be when you have to butcher/duplicate data structures in Coq to pass the totality checker.
Often I see hard to understand APIs in dynamically typed languages (see react-redux's 'connect' function) that end up having hideous type signatures. Other examples could be mixing commands and queries in a single procedure - see CQS as a good pattern that emerged from Eiffel.
1
I really need to spend more time practising CQS
1
Show replies
Except that tools are often much weaker than humans, because they're limited to a particular logic/proof method/etc. And sometimes a tool can brute-force something a human can't. So there's a fair bit that's not in the intersection, I think.
1