> I think many people question that they are good ideas. Not pure functions -- but forcing all functions to be pure. If you do that, you are basically forced to use monads for all effects, and that is very questionable.

You aren't forced to use monads specifically. What you're forced to do is distinguish pure from impure computations somehow. In the CBPV papers, it's clearly explained that functions are just one particular kind of computation. In CBPV, there's an adjunction between the categories of value types and computation types, and it's this adjunction that gives rise to a monad [corresponding to the effect(s) that computations might exhibit]. If we consider pure computations only [no effects, not even nontermination], this adjunction is actually an equivalence of categories.

---

> Yeah, Rust does something nice, too, but every operation allowed by Clojure is also allowed by Rust. I don't see how it's any better. Erlang's "let it crash" has nothing to do with data-race bugs.

I'm not talking about data races. Of course the absence of sharing in Erlang frees you from data races. But they don't free you from breaking transactional invariants, such as "this doesn't even begin happening unless that condition is met". In spite of the absence of data races, Erlang is still about coping with failure, not outruling it. In Rust, you can use a nonforgeable witness that the precondition holds, and consume it when the operation begins. It's rare that a non-dependently typed language is better than Haskell at something other than performance, but that's exactly what's happening here.

> Once you have a GC everything is a lot easier when it comes to concurrency. Rust works very hard to ensure safety without a GC, which is necessary for domains that can't use GCs (like programs in constrained environments).

Garbage collection makes sharing easy. However, concurrency control (i.e., controlling access to shared mutable resources) remains just as hard. Otherwise, nobody would have invented such things as "global interpreter locks".

> And in any case, I think most people would consider Rust to be even less functional or more imperative (whatever that means) than Clojure.

Indeed, Rust isn't terribly functional (though it's more functional that meets the eye), which is exactly why I said it's a better argument for "there are other ways besides functional programming".

---

> I also challenge you to program the world's most used sorting algorithm, TimSort, with equational reasoning.

Well, in order to use equational reasoning alone, I need a purely functional algorithm.

> And consider this -- Haskell is grossly insufficient to really reason about programs in this way. Idris is the very minimum to even start, and even that doesn't even begin to scratch temporal logic.

Haskell's type system is insufficient to verify equational reasoning using the type system, but equational reasoning is so simple that programmers can do it manually anyway. [More on this later.] On the other hand, programming languages based on dependent type theory, like Idris, while often more beautiful, and certainly more powerful, don't yet pass my bang for the buck test for everyday programming: (0) They force me to annotate things that Haskell can infer on its own. (1) It is a royal pain in the ass to manually translate data between representations that are convenient for proving [e.g., Peano naturals] and representations that are efficient for calculating things at runtime [e.g., machine integers, big integers]. (2) Most dependently typed languages often don't have terribly efficient implementations. To the best of my knowledge, ATS is the only honorable exception to the last point.

---

> That is a mathematical argument. Not a psychological one. You could use the same argument to claim that teaching a person to catch a ball is easier if you teach them Newton's equations than let them practice.

Your analogy breaks when you think about it non-superficially. Merely understanding the laws of physics won't make your muscles strong enough, or your reflexes fast enough to go out there and actually catch a ball. On the other hand, when you've written a program alongside its proof of correctness, well, you've written a program!

---

> Yes, imperative programming is too complicated for machines to verify in every circumstance, yet claiming it is too complicated for humans pretty much ignores reality (or, at the very least, requires some serious explaining).

It's too complicated for humans to verify too. If it weren't, more people would be doing it casually. This is unarguable, unless you've tried it yourself.

> even with security, memory safety has done a lot to make things better, and where it hasn't, dependent types would be necessary to prove correctness, anyway.

I never said that everything has to be machine verified. If you give me a proof that I can understand (i.e., I'm confident I can correctly verify), that's more than enough for me. But, if the proof is past a certain complexity threshold, I'll ask you to convince someone else that I can trust (a better mathematician or a proof assistant).