Propositions as Types

Propositions as Types, Philip Wadler. Draft, March 2014.

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.

Philip Wadler has written a very enjoyable (Like busses: you wait two thousand years for a definition of “effectively calculable”, and then three come along at once) paper about propositions as types that is accessible to PLTlettantes.

Wirth Symposium

Celebrating Niklaus Wirth's 80th Birthday, 20th Feb 2014.

Niklaus Wirth was a Professor of Computer Science at ETH Zürich, Switzerland, from 1968 to 1999. His principal areas of contribution were programming languages and methodology, software engineering, and design of personal workstations. He designed the programming languages Algol W, Pascal, Modula-2, and Oberon, was involved in the methodologies of structured programming and stepwise refinement, and designed and built the workstations Lilith and Ceres. He published several text books for courses on programming, algorithms and data structures, and logical design of digital circuits. He has received various prizes and honorary doctorates, including the Turing Award, the IEEE Computer Pioneer, and the Award for outstanding contributions to Computer Science Education.

We celebrated Niklaus Wirth's 80th birthday at ETH Zürich with talks by Vint Cerf, Hans Eberlé, Michael Franz, Bertrand Meyer, Carroll Morgan, Martin Odersky, Clemens Szyperski, and Kathleen Jensen. Wirth himself gave a talk about his recent port of Oberon onto a low-cost Xilinx FPGA with a CPU of his own design.

The webpage includes videos of the presentations.

Oral History of Adele Goldberg

Interesting and wide-ranging interview with Adele Goldberg from Computer History
Transcript and Video at Computer History Also on YouTube

Adele Goldberg reflects on her life and career from her early days at the University of Chicago and Stanford University through her career at Xerox Palo Alto Research Center (PARC) and ParcPlace Systems.

Another Oral History interview with her by IEEE Global History Network

Goldberg discusses her educational and work history. She recalls her experiences as a student at the University of Michigan and at the University of Chicago. Next, she covers her stretch at Xeorx PARC, sharing her views on the work environment. Here she speaks at length about her work on Smalltalk, including her leading role in its commercialization. Goldberg is candid about the challenges she faced in forming and running spin-out company ParcPlace Systems. In addition, she discusses her two-year tenure as President of ACM. Finally, Goldberg offers advice for young women who are considering a career in computing.

The origin of zero-based array indexing

An amusing historical analysis of the origin of zero based array indexing (hint: C wasn't the first). There's a twist to the story which I won't reveal, so as not to spoil the story for you. All in all, it's a nice anecdote, but it seems to me that many of the objections raised in the comments are valid.

John C. Reynolds, 1935-2013

Randy Bryant, dean of the school of computer science at CMU, sent out an email saying that John C. Reynolds passed away yesterday.

Subject: In Memoriam. John Reynolds, June 1, 1935 - April 28, 2013
Date: Sun, 28 Apr 2013 21:45:12 -0400
From: Randy Bryant
To: scs-all@cs.cmu.edu

I'm sorry to announce that John Reynolds, a long-time member of our computer science faculty, passed away early this morning. Many of you know that John had been in declining health recently. We were able to celebrate his retirement him last summer. He had a heart attack last week and went downhill over a period of several days.

John got his PhD in 1961 in theoretical physics, but while working at Argonne National Laboratory came to realize that his passion was for computation. He became a very successful computer scientists, focusing on the logical foundations of programs and programming languages. He was at Syracuse University from 1970 to 1986 and then joined the CSD faculty.

John has made many important contributions over his career. Interestingly, his 2002 work on separation logic, done jointly with Peter O'Hearn and others, has been especially prominent. Separation logic provides a formal way to reason about what we might think of as "normal programs," i.e., ones that operate by changing the values stored in memory, but where memory is partitioned into independent blocks, and so we can reason about different program components independently. I can only hope that the work I do at age 67 would be counted among my best!

We will also remember John for this cheerful spirit, his high ethical standards, and his deep intellect. He will very much be missed.

Randy Bryant

It's probably impossible to overstate the impact that John had on the field of programming languages. But beyond being a great scholar, he was also a generous mentor and a fundamentally decent and kind human being. He will indeed very much be missed.


I was surprised to see that DYNAMO hasn't been mentioned here in the past. DYNAMO (DYNAmic MOdels) was the simulation language used to code the simulations that led to the famous 1972 book The Limits to Growth from The Club of Rome. The language was designed in the late 1950s. It is clear that the language was used in several other places and evolved through several iterations, though I am not sure how extensively it was used. When Stafford Beer was creating Cybersyn for Salvador Allende he used DYNAMO to save time suggesting it was somewhat of a standard tool (this is described in Andrew Pickering's important book The Cybernetic Brain).

The language itself is essentially what you'd expect. It is declarative, programs consisting of a set of equations. The equations are zero and first-order difference equations of two kinds: level equations (accumulations) and rate equations (flows). Computation is integration over time. Levels can depend on rates and vice versa with the language automatically handling dependencies and circularities. Code looks like code looked those days: fixed columns, all caps, eight characters identifiers.

Here are a few links:

  • Section 3.7 of this history of discrete event simulation languages is a succinct description of the history of the language and its main features.
  • A more leisurely description of the language and the Limits to Growth model can be found in this article. Ironically, the author of the article reimplemented the model in Javascript (run it!). What was originally written in a DSL is now implemented in a general purpose language, with all the niceties handled manually.
  • Finally, a nice piece on Jay Forrester who prompted the creation of SIMPLE and DYNAMO, its offspring.

Photoshop 1.0 Source Code

Some people are amazed that it's in Pascal... HN discussion is here.

Milner Symposium 2012

The Milner Symposium 2012 was held in Edinburgh this April in memory of the late Robin Milner.

The Milner Symposium is a celebration of the life and work of one of the world's greatest computer scientists, Robin Milner. The symposium will feature leading researchers whose work is inspired by Robin Milner.

The programme consisted of academic talks by colleagues and past students. The talks and slides are available online.

I particularly liked the interleaving of the personal and human narrative underlying the scientific journey. A particularly good example is Joachim Parrow's talk on the origins of the pi calculus. Of particular interest to LtU members is the panel on the future of functional programming languages, consisting of Phil Wadler, Xavier Leroy, David MacQueen, Martin Odersky, Simon Peyton-Jones, and Don Syme.

Common Lisp: The Untold Story

Common Lisp: The Untold Story, by Kent Pitman. A nice paper about the history of my favorite lightweight dynamic language.

This paper summarizes a talk given at “Lisp50@OOPSLA,” the 50th Anniversary of Lisp workshop, Monday, October 20, 2008, an event co-located with the OOPSLA’08 in Nashville, TN, in which I offered my personal, subjective account of how I came to be involved with Common Lisp and the Common Lisp standard, and of what I learned from the process.

Some of my favorite parts are:

  • How CL was viewed as competition to C++. (Really, what were they thinking?)
  • How CL was a reaction to the threat of Interlisp, and how "CLOS was the price of getting the Xerox/Interlisp community folded back into Lisp community as a whole" (link).
  • How individuals shaped the processes of standardization. MIT Sloan did an analysis of these processes.
  • How the two- to three-day roundtrip time for UUCP emails to Europe may be responsible for the creation of the separate EuLisp.

I have a soft spot for CL, so I am biased, but I think Greenspun's Tenth Rule (and Robert Morris' corollary) still holds - CL is the language that newer dynamic languages, such as Perl 6, JavaScript, and Racket are asymptotically approaching (and exceeding in some cases, which is why I view CL as a lightweight language today.)

Dennis Ritchie passed away

I have just learned that Dennis Ritchie (1941-2011) has passed away. His contributions changed the computing world. As everyone here knows, dmr developed C, and with Brian Kernighan co-authored K&R, a book that served many of us in school and in our professional lives and remains a classic text in the field, if only for its style and elegance. He was also one of the central figures behind UNIX. Major programming languages, notably C++ and Java, are descendants of Ritchie's work; many other programming languages in use today show traces of his influences.


Bjarne Stroustrup puts the C revolution in perspective: They said it couldn’t be done, and he did it.

XML feed