> Why is this taken as a given to be a good thing? So that we can prove things about software more easily. If we only write stateful imperative programs, we're

> Why is this taken as a given to be a good thing? So that we can prove things about software more easily. If we only write stateful imperative programs, we're stuck with tons of Hoare triples and separation logic rather than being able to use equational reasoning or type-driven deductions. For example, this person wrote a parallel wc in Haskell, and they used semigroups to parallelize the word counting. https://chrispenner.ca/posts/wc https://chrispenner.ca/posts/wc