I disagree. I think reasoning in a programming language that limits effects with types and promotes partitioning them from the rest of your logic is dramatically simpler than in languages where mutation and effects can happen anywhere.
That's a red herring and a scare-story that FPers tell each other. They can't happen "anywhere". They happen where you tell them to happen.
Do you have any evidence that actual reasoning is simpler?
"At the end you usually get a tight loop that is easy to follow. It is also much more imperative/operational than before, which may bug Haskell-style people." -- Jonathan Blow
This matches my experience pretty well. When I first created Higher Order Messaging, I was also really into creating chained higher order ops. After a little while, I noticed that a small for-loop was actually more readable than the really cool filter-chains I had created. Less cool, but more readable, comprehensible, easier to reason about, not least because of named intermediate values, something that tends to get lost in point-free style (and trust me, having been a heavy user + implementor of Postscript, I know a little about point-free style).
In a strongly typed functional program I can prove that side effects only happen in specific places that are designated by the types. I have no such assistance in say Java, or Python. That is what I mean that side effects can happen anywhere.
I would call referential transparency, which gives rise to equational reasoning, very strong evidence that reasoning becomes simpler.
You're still conflating "prove" with "reason". I don't need to prove things about my code in order to reason about it. For example, I can just look at the code in question to know whether it has side effects, and most code doesn't.
In fact, most proofs I have seen don't particularly help me reason about the code in question. On the other hand, a simple imperative execution model does help me reason about the code.
Being able to reason about things equationally makes my code easier to reason about. Having a type system and a compiler assist me makes my code easier to reason about. Having fewer variants makes my code easier to reason about. Not needing to know the order in which functions have been invoked to know their return values makes my code easier to reason about.
However, I will make the statement -- and this is indeed conflating! -- If I can prove something about my code, then it is easier to reason about. The proof can be simple or complex.
Again, you are just repeating your assertions and somehow think that simply asserting them makes them true. It does not, and I don't think I can make you understand the difference between assertions and evidence, so let's call it a day.
I think my assertions are pretty well accepted virtually ... everywhere, so it didn't really occur to me THOSE specifically were what you were calling into question. But if THAT is what we are arguing about, I agree, this is all rather cyclical and pointless.
They're not. Or rather, you have a very narrow definition of "everywhere". And even if they were, that doesn't make them true without evidence, quite the contrary, that makes them especially suspect (groupthink etc.). Also, if you're so sure they are universally accepted, why the need to argue them at all? And of course, if they are so universally true, it should be trivial to actually come up with actual evidence, which hasn't been the case.
