I depart from this paper in that I need to compare capabilities, not objects.
The paper feels it needs an equivalence relation on capabilities that asks if two capabilities designate the same object, all be it with different permissions.
My answer to this question is no: there should not be such a primitive query on two caps.
Here is why I say no:
If code defining some class of objects wants to support a query, including a capability X, which asks “Is X your sibling?” or equivalently “Did your creator create X?”, that code can certainly do so.
I somewhat object to the syntax of some language committing me to answer such a question for I am not sure that it is always compatible with the intended object semantics.
Further I want a binary predicate ‘=’ that guarantees x=x despite the behavior of the code defining x.
In short the left handed equal is too much and too little for my purposes.
It may indeed be useful however.
Factories vouch for each other not for an equivalence relation, but for a partial ordering of discretion.
Who is responsible for insuring that the left handed query has no side effects?
I think there is no one responsible who we can rely on.
If I imagine that I may have two slots each with a capability, I want to know if they hold the same cap even when I don’t trust the code defining the behavior of the object they would designate in that case.
I need a primitive which ensures that x=x without depending on whatever x designates.
All these techniques depend on an object’s clients being unable to distinguish between the identity of the naked underlying object, and that object wrapped within an encapsulator (proxy, chaperone, impersonator).
I propose, but have not proven that this is not a danger for a membrane separates the real from the fake and those who you fear will be able to discriminate will never hold both caps.
I might be able to find a proof, or those who disagree might be able to find a concrete case.
I think neither has happened.
My case is pretty clear for the wire protocol.
Drossopoulou and Noble write “o obeys S” to represent an assumption that an object o conforms to a specification S.
Their contribution is that this trust is an assumption, not an assertion: obeys does not mean that o conforms to that specification, but that we will proceed as if it did meet
the specification.
I object to this.
Whether a proposition is a theorem or hypothesis is not wrapped up in its syntax but in the surrounding meta language.
I like their “obeys” but I take it as a proposition.
We can prove it whence it becomes a theorem, or assume it whence it becomes an hypothesis.
I am trying to understand ‘autognosis’ from the paper.
Can Mark Miller’s ‘mint maker’, be done autognostically?
It sounds to me as if such a language prohibits siblings from recognizing each other.
One of the few things I like about C++ is the efficient synergy (compile time) which allows an object to access the innards of a sibling to which it holds an otherwise opaque reference.
(I am not now sure which language C++ got this from. I once thought I knew.)
Warning: philosophical stance:
I am of the school that, when discussing language semantics, distinguishes between an integer and a mutable cell that holds that integer.
I understood the distinction profoundly for the first time perhaps when I learned to read the Algol 68 document.
Some of the authors quoted in the paper seem unable to make that distinction.
They wonder what = should mean.
Consider the two valid distinct C routines:
int eqA(int * a, int * b){return a==b;}
int eqB(int * a, int * b){return *a==*b;}
C makes the distinction.
C is in charge of the semantics of both b and *b and thus there is no problem.
I suppose the idea is that an object represents something that language semantics cannot grok.
Suppose we have an object that somehow denotes the shape of a flower.
Fine. I still need to ask if two flower objects are the same, if only to sometimes avoid asking the objects if they ‘denote’ the same shape.
Does autognosis preclude this?
To what end?
It sounds like ruling out eqA above.
May we use the qualities of reflexivity, transitivity and symmetry of equal?
(X=X; (X=Y & Y=Z → X=Z); X=Y → Y=X)
I think I need those properties to reason about algorithms.
If so what code is responsible for ensuring this.
Shapiro adds:Bigger issue: to implement "ask x about y" you either need a guarantee of memory less confined behavior or you have to trust X not to misuse the Y capability.
It is even worse: Even with confinement, you trust X not to invoke Y in a damaging way.
In some situations you know and trust the behavior of X and wonder about a new Y.
I think that capability distribution needs more and I am trying to prove that.
I have no objection to compilers that use “under the cover pointers”, or even languages that seem to require such subterfuge.
(Algol’s flexible arrays)
Those are well hidden and do not impact reasoning about program meaning.