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
