On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote: > Most languages have not been proven sound. I know ML has been, and there > is a reduced version of Java (Featherweight Java) that has been proven > sound. I know that Java with generics has been shown unsound a long time > ago > (http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html) > . I haven't followed to see whether that issue has been fixed. My > understanding is that as of this time Java with generics is still > unsound, i.e. there are programs without casts that produce type errors > at runtime.
Thanks to reflection, it wouldn't be all that hard to shove the wrong type into a container with code that can't be properly checked at compile time. Since all the generic stuff is simply compile-time checks, the compiler fails to catch the problem, and all of the code which compiled with the assumption that the objects in the container were all of one type will fail when it goes to get the item with the wrong type out of the container. I think that all of the casts are still there though (since technically, the container holds Objects not the specific type). It's just that they aren't in the user code. In reality, this sort of thing pretty much doesn't happen, because you have to go out of your way to make it happen, but as far as proofs go, it's definitely going to fail. - Jonathan M Davis
