• Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> Aug 25 2009
• Kagamin <spam here.lot> Aug 26 2009

Andrei Alexandrescu <SeeWebsiteForEmail erdani.org> writes:

Depending how you look at this, it is either a success or a failure of 
formal methods in designing programming languages.

http://twofoos.org/content/java-type-system-holes/

I didn't know about this. Loopholes in Java have come up now and then, 
but I thought they'd fixed them all. An older one (2001) was this:

http://fpl.cs.depaul.edu/Problem.java

Igarishi, Pierce and Wadler had shown (OOPSLA 1999) that Java's core 
type checking is correct, but have not included a host of generics in 
the proof. Apparently that's still a problem.


Andrei

Kagamin <spam here.lot> writes:

Andrei Alexandrescu Wrote:

 Depending how you look at this, it is either a success or a failure of 
 formal methods in designing programming languages.
 
 http://twofoos.org/content/java-type-system-holes/


As to the first bug, it's clearly a runtime bug, not language's. It's stated
that this bug is detected by the compiler when it's possible.