Lambda the Ultimate

An old POPL paper from 1982:

We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel. Partition Types to Predicate Types. Computable to Definable, and Syntactic Consistency to Semantic Consistency. We argue for the adoption of each. We exhibit a programming language, Viron, that capitalizes on these shifts.

Summaries of the shifts (from paper):

• From Effect to Entity. Large objects are made as mobile as small, so that they can be easily created, destroyed, and moved around as entities instead of being operated on piecemeal as a static collection of small objects.
• From Serial to Parallel. Constructs intended for parallel computation are also used to subsume both serial and data constructs, achieving a simplification of the control structures of the language as well as providing a framework for organizing the data structures.
• From Partition Types to Predicate Types. The partition view of types partitions the universe into blocks constituting the atomic types, so that every object has a definite type, namely the block containing it. The predicate view considers a type to be just another predicate, with no a priori notion of the type of an object.
• From Computable to Definable. Effectiveness is a traditional prerequisite for the admission of constructs to programming languages. Weakening this prerequisite to mere definability expands the language’s expressiveness thereby improving communication between programmer and computer.
• From Syntactic Consistency to Semantic Consistency. Consistency is traditionally enforced by syntactic restriction, e.g. via type structure. A recently developed alternative popularized by Dana Scott takes the dual approach of resolving inconsistencies via semantic expansion as done for models of the untyped lambda calculus. We argue that the latter approach simplifies language structure.

Nothing like that could get into POPL anymore :) What are the paradigm shifts going on today?

[Church 1934] stated the fundamental paradox as follows:

"in the case of any system of symbolic logic, the set of all provable theorems is [computationally] enumerable... any system of symbolic logic not hopelessly inadequate ... would contain the formal theorem that this same system ... was either insufficient [theorems are not computationally enumerable] or over-sufficient [that theorems are computationally enumerable means that the system is inconsistent]...
This, of course, is a deplorable state of affairs...
Indeed, if there is no formalization of logic as a whole, then there is no exact description of what logic is, for it in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic."