Axiomatic purity of D

[Andrei Alexandrescu]

On 08/01/2010 06:02 PM, 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.

Good point. Reflection is commonly avoided in the kind of formal proofs 
I mentioned.

Andrei