[catnaroek]

> It doesn't try to analyze and compare existing programming languages.

It does. For example, this theory identifies when and how incorrectly designed programming languages fail to enforce abstractions, very much like how the theory of database normalization identifies when and how incorrectly designed database schemata fail to enforce data integrity constraints.

But perhaps what you mean is “it doesn't try to view existing programming languages under an unwarranted positive light”.

[pron]

Programming language theory has no concept of "correctly-" or "incorrectly-designed." It may show some properties of some languages, and researchers may express their opinion that they believe those properties are inadvisable for programmers. Programming language theory does not define a metric for what's good or bad, and, in fact, programmers are often (though not always) better judges of that than theorists.

[mbid]

I certainly didn't mean to imply that the programming languages ignored by these reasearchers are any good, on the contrary. It's just that I find the way these researchers sell themselves questionable. They don't have a theory of programming languages, they have a theory of some variant of the lambda calculus. It would be more honest to call it just that.

[empath75]

The lambda calculus is a very simple set of rules which is Turing complete— whichever kind of programming language you prefer can be broken down to lambda calculus.

[mbid]

Let me clarify---some version of typed lambda calculus. The document linked here doesn't seem to deal with the untyped lambda calculus and much less so with properties that are stable under change of representation of computable function.