My point was that it's possible to systematically extend (or restrict) the lambda calculus and associated techniques. You can add effectful operations and give them semantics (e.g. as functions on stores), define a cost semantics and prove whatever you want while being completely formal.
Try extending RAMs with dynamic allocation, call stacks, or anything to make it more natural to write down a whole algorithm. Try proving something about the composition of RAM programs. I don't think you'll get very far.
There are many interesting algorithms that are usually analyzed in an imperative setting, like in-place quicksort, Knuth-Morris-Pratt, or Gaussian elimination. There doesn't seem to be any benefit to analyzing them in an FP setting, because it's not easier and doesn't yield new insights.
It seems to me that the FP approach only really shines on algorithms that are "naturally tree-like". For example, I'm a big fan of Okasaki's work on purely functional data structures, and of Blelloch's work-depth model. But let's not oversell FP techniques as the foundation of all algorithm work.
The field that gave rise to FP has a lot to say about how we specify languages and their properties and how we prove things about programs in general. That includes languages with all kinds of effects: state, exceptions, concurrency, etc, and equally as imporant, mechanisms for abstraction and modularity. There's currently no other "foundation" for computation that lets us define these ideas formally.
In discussions of FP, the contributions of the field get reduced to "programming with functions".
Elsewhere mafribe mentions parallel processing... which is also clearly in another class.