Lambda the Ultimate

Niklaus Wirth discusses two of his Pascal successor languages in the HOPL-III paper on Modula-2 and Oberon.

This is an account of the development of the languages Modula-2 and Oberon. Together with their ancestors ALGOL 60 and Pascal they form a family called Algol-like languages. Pascal (1970) reflected the ideas of Structured Programming, Modula-2 (1979) added those of modular system design, and Oberon (1988) catered to the object-oriented style. Thus they mirror the essential programming paradigms of the past decades. Here the major language properties are outlined, followed by an account of the respective implementation efforts. The conditions and the environments are elucidated, in which the languages were created. We point out that simplicity of design was the most essential, guiding principle. Clarity of concepts, economy of features, efficiency and reliability of implementations were its consequences.

The main influence on these languages were the Xerox Parc languages of Mesa and Cedar (which were Pascal derivatives). Mesa and Modula-2 explored modules, while Cedar and Oberon were concerned with the entire operating system experience. As Wirth states a couple of times in the paper, his main goal was to teach programming concepts, using language design to further that end, but with an eye for use in non-academic settings. He frowns on the design of modern PLs, with its lack of resource constraints and kitchen-sink approaches - expressing concern that it makes it hard to teach structured programming. He also expresses concern that operating systems are no longer a subject of research, much less integration with PL design.

(Previous LtU links to HOPL-III papers.)

I am by no means deeply educated in regards to category theory, but I wanted to see if my thinking is on the right track.

Can I construct a category consisting of propositions as its objects and inference rules as structure preserving morphisms between these objects? Does this category in some way offer an operational semantics for a top level predication that asserts this complex of propositions?

This is probably not a new idea, it was one of those things I just felt like working through myself, but it ended up taking way too much time.

Two stacks for tail calls gives a different approach to tail call optimization than the ones I was able to find, and my hunch is that's because it doesn't improve that much. But I still think it's a neat idea, maybe someone else will too.