Sandro, I have to ask how important it is to you that I continue responding to your points and questions. It seems like you at least understand what I'm saying, although you clearly have a very different opinion about it. I don't need to convince you and I'd really rather stop discussing it now. All this back and forth doesn't seem to be changing anyone's minds. It may be that I'm still abusing a few terms, but that's not the heart of it. I think if we really want to fully explain ourselves at this point, the best way would be to go through a number of examples in detail. But I don't see why that's worth the trouble, since this issue is not an issue for BitC in the near term, or maybe ever.
On Tue, Jul 8, 2014 at 12:05 AM, Sandro Magi <[email protected]> wrote: > On 07/07/2014 9:16 PM, Matt Oliveri wrote: >> It's rights amplification only when we consider static types to >> provide information about permissions or authority. > > In an object-oriented language, you are permitted to send objects > messages. In a typed object oriented language, you are permitted to send > messages only to objects that can receive those messages (as defined by > some criteria). Types must carry permissions, in principle. > >> Technically you can't say which of the two is more precise. Because >> they contradict each other, neither can be a refinement of the other. > > My view yields strictly more precise information at every point in the > program, so I disagree that neither view subsumes the other. > > Certainly they have inconsistent ontologies, but your view doesn't > capture the subjective experience of programming in Java. Dynamic > message sends don't look anything like native static message sends for > one, so Java is not like any other dynamically typed language in > existence. And to argue that some operations are disallowed, but they > aren't disallowed by some system of "permissions" seems bizarre > (consider refinements of Java's type system like adding typestate where > the state of a file handle is in the type -- now types suddenly do > define permissions?). > >> Indeed, it is because downcast would otherwise provide uncontrolled rights >> amplification that we must not consider static types as limiting authority. >> [...] My position allows static types, ambient reflection and downcast, and >> the object-capability model to coexist. > > I don't understand. Nothing about my perspective forbids a capability > secure language from having some forms of rights amplification, as long > as they are "sufficiently benign". For instance, some capability > languages include rights amplification in the form of EQ. > > Language security is not necessarily all or nothing, but often a sliding > scale, ie. less rights amplification = more secure by default. No one > ever said "any rights amplification = insecure". Java isn't capability > insecure simply because some forms of rights amplification are > available, it's insecure because it violates the connectivity postulate, > and the encapsulation postulate given unrestricted reflection. > > We can still recognize that Joe-E is capability secure, even though it > includes rights amplification in the form of downcasts and (restricted) > reflection. This isn't inconsistent with my view in any way, we simply > recognize the rights amplification for what it is. > > Sandro _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
