Here's an answer to that:

https://www.quora.com/Why-is-functional-programming-suited-f...

Functional programming is also easier to mathematically verify than imperative:

https://semantic-domain.blogspot.com/2018/04/are-functional-...

While you might not do proof, languages and methods that are easier for proof are often easier for automated analyses that look for problems, too. There's tools out there that can check code for concurrency problems that are extremely hard to spot with just testing. They might be easier to build or get more results if the program was functional/stateful instead of heavily stateful.

this is how you end up with darcs as your version control system. It’s provably correct, but about 1 in 10 times it hangs forever and never terminates. Also it doesn’t implement branching because that’s out of scope for the model.

Nah, it's how you end up with HACL*: verified crypto that performs like C shipping in Firefox.

https://github.com/project-everest/hacl-star

You can verify stupid designs or smart ones. You can do impractical verification or pragmatic approaches. Formal verification is a tool whose outcomes depend on who wields it. The only consistent drawbacks it has are requiring more expertise, the project takes longer, and the project has to be simplified in design/implementation. High-quality software in general (eg OpenBSD) often has same properties, though. Possibly intrinsic to achieving correctness rather than additional requirement of formal methods.

I think you're mixing the result of implementation and the way something's implemented. Darcs relies on abstract theory which implemented didn't end up very performant or full of features. But it would be close to the same speed if it was implemented in terrible C. On the other hand you can write provable implementation of git with similar speed as the current one.

Not having shared memory eliminates a whole host of popular errors in concurrent languages; handling messaging explicitly as messaging forces an ordering on events, which is nice too.

Of course, you can still deadlock yourself; and read-modify-write can still be done in a racy fashion. Emergent properties of a system are still hard to reason about, but individual processes should be easy to reason about.

Problems like #2 are all about emergent behavior problems, so thinking through 2nd and 3rd order effects. Isolating things in stateless functional units and using higher level constructs doesn't actually gift the engineer with the foresight to think through these problems. I agree with GP, these problems are orthogonal from using FP or OOP.