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
