[l_dopa]

> I'd like the "foundation" of CS to give a faithful mathematical description of what computers can and cannot do. Is that too much to ask?

http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

> A better "foundation" would try to describe computational behavior and reason about it, instead of abstracting it away

A lot of interesting research does exactly this, and a lot of it has found its way into ML-family languages. The starting point (or "foundation") in every case is a typed lambda calculus. Machine models, like turing machines, are just annoying to reason about and not extensible in any meaningful way.

[cousin_it]

Alas, the Church-Turing thesis doesn't say that every imperative algorithm can be translated to lambda calculus while keeping the same time and space complexity. The two main culprits are in-place mutation and O(1) array indexing.

[l_dopa]

Sorry for the glib answer. I'm not arguing for programming in the pure, untyped lambda calculus.

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.

[cousin_it]

Maybe we're talking about slightly different things?

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.

[l_dopa]

Yes, we're talking about different things. I took the parent comment to mean that talking narrowly about "FP" as programming with pure functions isn't very useful any more. It may have made sense in the 90s when few widely-used languages had h.o.f, but that fight has pretty much been won.

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".

[tel]

It doesn't even say that any imperative algorithm can be translated---merely Turing Machine algorithms which also don't happen to have O(1) array indexing, e.g..

Elsewhere mafribe mentions parallel processing... which is also clearly in another class.