Axiomatic purity of D

[Jonathan M Davis]

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