These are my comments on section 6 of:
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.
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.