Axiomatic purity of D

[retard]

Sun, 01 Aug 2010 16:02:56 -0700, Jonathan M Davis wrote:

> 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

If you restrict yourself to a subset of the language with no casts and no 
pointer manipulation, all kind of safety properties of the polymorphic / 
generic containers can be proven. There is even a "safe" version of casts 
known as pattern matching in languages like Scala. However, if the class 
hierarchy isn't sealed, one cannot prove whether the pattern matching 
function is total. There are also other issues with patterns because of 
the type erasure in JVM.

Sounds like Andrei might have read the brick wall book by B.P. It's a 
basic book about language design (orthogonal to the parsing/backend books 
like the one with the dragon in its cover) and an essential part of grad/
postgrad studies in many places. It's a good read they say.