Lambda the Ultimate

Active link: New paper: Theory of Programs

From the link:

"One of the principal ideas is that a program is simply the description of a mathematical relation. The program text is a rendering of that relation. As a consequence, one may construct programming languages simply as notations to express certain kinds of mathematics. This approach is the reverse of the usual one, where the program text and its programming languages are the starting point and the center of attention: theoreticians develop techniques to relate them to mathematical concepts. It is more effective to start from the mathematics (“unparsing” rather than parsing)."

We already saw that the first attempt, stating that specifications are abstract and programs concrete, does not make the cut, since “level of abstraction” is a relative notion (the example was an assignment instruction, abstract for some and concrete for others). A seemingly more promising intuition is that programs are executable while specifications are purely descriptive. But that is also not right, even if we ignore the case frequently made for “executable specification” formalisms and stick to more traditional forms of the concepts. “Executable” cannot mean “directly appropriate for execution on a computer”, since in that case the notion would depend on hardware details. It has to mean “expressible in a programming language’. A staple example is that Result^2 = input is a specification whereas a particular square root computation, using for example Newton’s algorithm, is a program. But such examples also fail, since there are many programming languages today in which you can just write Result^2 = input and let the compiler figure out the implementation.

I didn't find this argument very compelling. 'Executable' is exactly what distinguishes a program from mere specification the way I use the terms. In some languages, x^2=y defines an effective procedure for computing x, and in other languages it doesn't. In the former, it's a program. In the latter, it's a specification.

It was an interesting read, though. Thanks for posting.

I haven't finished reading the paper, but the mathematics seemed indeed sound and much more elementary than in other works. I'm not sure it's more elementary than Hoare logic — if anything, more standard. In any case, I'd like to understand what's the simplifying insight. I'm not an expert, but "other stuff was just unnecessarily complicated" sounds an unlikely explanation. "Other stuff also achieved X, Y and Z, but we consciously give them up because $reasons" would be more credible.

I've also read the discussion on axiomatic methods in Sec. 6.1, and it doesn't seem accurate. Let me quote:

[Talking about Hoare logic using axioms] admirable work of Hoare and colleagues [7][8]. A notable property of these efforts is that they postulate their laws [...] The justification for this method — postulate your ideal laws, the model will follow — is that it has, in Russell’s words cited in [9], “the advantages of theft over honest toil”.

That quote from Russell appears too strong — after admiring Hoare's work, it compares it to theft.
First of all, this section seems to miss that people have proved Hoare logic sound wrt. other semantics.
More in general, tons of literature defines axioms and propose different models for those axioms. Those axioms serve as an interface for the different models. Similarly, you only run actual implemented methods, yet interfaces and abstract methods have a role.

However, sometimes interfaces make a system harder to understand. Removing indirection can make a system easier to understand, and maybe that's what this paper is doing as well.