[Grace-core] Minutes of Teleconference 23-24.8.12

[Bart Jacobs]

On 27/08/2012 10:09, James Noble wrote:
> that reminds me that we should look at other aspects of the language design which may help (or hinder) verification.
>
> The only obvious one I can think of is named result variables - Pascal had a named variable that is returned,
> so post-conditions can name that variable - I think Eiffel does something similar?  Go is bringing back names
> for return values, too.
>
> But I'm sure there must be others!

I haven't noticed any major issues so far; 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.)

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.)

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.

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.

Bart


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm