[Grace-core] Minutes of Teleconference 23-24.8.12

[James Noble]

On 27/08/2012, at 22:46 PM, Bart Jacobs wrote:

> I haven't noticed any major issues so far;

good!

> I think a reasonably usable verification tool can be built for Grace (even without the type system). (I started hacking up a minimalistic prototype (in Grace) some time ago; I should finish it at some point.)

oh cool! yes that would be great. If there's stuff we can do to help, let us know.
(hmm, we really should plan on a proper Grace workshop at ECOOP next year, then)

> The biggest potential issue that I see is the apparent brittleness of "downcasting" based on structural types. By "downcasting", I mean that things (such as the behavior of methods) are assumed about an object based on its structural type. This mechanism seems more brittle than the classical nominal types-based approach, where (fully qualified) nominal types are usually long and robust, in the sense that clashes are less likely, and furthermore, there is a logical place to go look for the contracts associated with a nominal type. (E.g., the contracts for com.foobarcorp.MyWidget are supplied by FooBarCorp and are probably found on their website, or at least they ship with foobarcorp-widgets.jar.)

Right. Effectively you have to assume a single global space of method names.
There are other things you could do - a notably a lisp style namespace mechanism to give 
more structure, but we're trying not to buy into to that, at least not yet.

> I guess the way to verify code that performs such downcasts would be for the "common supertype" to specify a catalog of possible "subtypes" and their associated contracts. Note that this means that instead of matching against the structural type, one might as well (for verification purposes, possibly not for type checking purposes) match against some integer or string tag returned by a supertype method.

We have some thoughts about explicit brands that would give more support for this -
but haven't got very far yet. I think that kind of direction may be a minimal way of
getting most of the benefits of a hybrid nominal/structural type system -
without going to the Scala approach, or Donna Malayeri's Unity...
but we need to get the basics of the reified / generic / structural / gradual system going first...

> This "catalog" approach seems feasible, and in some ways more pure and logically elegant, but the nominal types-based approach seems more practical.
> 
> A related potential issue is in verifying code that interacts with untrusted code: when you get an object from an untrusted source in Java, if you cast it to String and the cast succeeds, you know how the object's methods will behave, since you know the object is implemented by the built-in class String. In Grace, there seems to be no way to positively establish the "trustworthiness" of an object (short of some kind of cryptographic challenge-response protocol??). I guess this was very much by design, but sometimes I think you really want to know who you're talking to.

right. yes, this is another important use-case, and again if we go to brands
that should address it nicely --- again with only a little delta to the underlying system

James