These are my comments on section 6 of: This paper introduces several new ideas to the realm of programming languages. Morris says a number of things better than I have in these pages. The paper appeared in 1973 as Keykos was in its early design stages. We would have learned from it had we read it. I think we eventually included its insights.

There is terminology in the paper that should be more broadly used. An object is ‘local to a region of program text’ if all access to that object occurs in that text as a simple matter of syntax. The objects that Morris has in mind are mutable objects such as a cell that can be stored into.

I reread the paper closely now (2016) wondering whether Morris specifies that the holder of the unsealer not have access to box content without the box.

I had mostly forgotten the language Gedanken. I am now surprised how much influence Gedanken had on the ML languages.


Just now I am rereading the Morris paper closely to see if he tries to justify needing both a sealed box and the corresponding unsealer to get the box content. Some might imagine that everything ever sealed by a given sealer ought be accessible to anyone with the matching unsealer. No; one must invoke the unsealer passing the box!

My first comment is that it has been too long since I read this paper and it says several things that I have said less well.

Morris provides some formalism in section 6 that I had not recalled that might help prove or disprove correctness of the Stiegler seal.