Back to the future

The programming language ALGOL was “a language so far ahead of its time, that it was not only an improvement on its predecessors, but also on nearly all its successors,” at least according to C.A.R. Hoare. Few programming languages have been more studied [this] or better understood semantically; perhaps a dozen variations on this language obtained by adding various features have known fully abstract semantic models, mostly using game semantics. Few programming languages have a better programming logic than Reynolds’s awesome ALGOL specification logic [this]. And Reynolds’s Syntactic Control of Interference type system for ALGOL is a very clever way to handle effects in functional programming languages, avoiding some of the complications of monadic type systems.

Yet nobody is actually programming in this amazing language. What a pity. Call-by-name is certainly a problem, but it is mainly a problem for compiler writers rather than programmers. If you stick with first order functions, which is most of the code one normally writes, it is straightforward to force evaluation. And who is smart enough to use higher-order functions should be smart enough to use them efficiently.

Our old-new programming language Verity is a pretty faithful version of ALGOL, with the syntax mildly modernized (type inference, etc). Right now we only use this language to do higher-level synthesis, but I think it deserves to grow into a more general purpose language.

About Dan Ghica

Reader in Semantics of Programming Languages // University of Birmingham // https://twitter.com/danghica // https://www.facebook.com/dan.ghica
This entry was posted in Geometry of Synthesis. Bookmark the permalink.

2 Responses to Back to the future

  1. What Dan says! Algol is extremely elegant; I make essential use of it in my PL textbook to discuss state and concurrency, and have recently been using it as a basis for work on information flow security with a student.

    In my formulation, which is subtly different from Reynolds’s, there is no reliance on call-by-name. Instead I have an explicit lax modality to encapsulate commands as values, and these can be passed by-value without difficulty or loss of expressiveness. More importantly, I depart from Reynolds in that assignables (my word for mutable variables, which I think is better) are not forms of expression. Rather, one must use a command to fetch the contents of an assignable and bind it to an actual variable before using it. I have not investigated what this change would do to specification logic, but given the messiness of Hoare’s logic in the treatment of assignables, I suspect it can only improve it (but that remains to be shown).

    • Dan Ghica says:

      If I may highlight from your book, this is precisely why I like Algol:


      L{nat,cmd ⇀} maintains a careful separation between pure expressions, whose meaning does not depend on any assignables, and impure commands, whose meaning is given in terms of assignables.

      How come no modern language manages to do that?

Leave a Reply

Your email address will not be published. Required fields are marked *

*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>