Re: failures

The original Java classloader design had a major bug -- arising 
basically (in my opinion) because of some naive reasoning by the 
language designers. See http://www.research.att.com/~vj/bug.html

After some careful thinking, this was subsequently fixed. See 

One could similarly argue that the entire Java Thread design (Chapter 
17) is substantially flawed. I have not personally spent time on it, but 
I know that Doug Lea and Bill Pugh are leading a major effort to 
redesign the Java Memory Model, see 


Martin Abadi wrote:

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> Another example, with a somewhat similar flavor, is the combination
> of subroutines and object initialization in the Java bytecode language.
> Both subroutines and object initialization are delicate even in 
> isolation.
> Freund and Mitchell found that the Java bytecode verifier (in Sun's
> JDK 1.1.4) did not treat their interactions correctly. More specifically,
> exploiting some loopholes related to subroutines, one could use an
> object before its initialization, contradicting the intended properties
> of the verifier.
> There might be a third example in the work of Gordon and Syme
> on typing the intermediate language in Microsoft's Common Language
> Runtime. Their paper says "The process of writing this specification,
> deploying the executable specification as a test oracle, and
> applying theorem proving techniques, helped us identify several
> security critical bugs during development." I don't remember seeing
> published details of those bugs.
> Martin
> Matthias Felleisen wrote:
>> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>> Okay, this didn't work out. Let's try again.
>> Are examples out there that show how naive reasoning about languages
>> (not individual programs) is a major problem?
>>   The canonical example is to combine polymorphic let without
>>   restrictions with naive generalizations for references, exceptions,
>>   continuations, and channels.
>> For what else have we needed *any* form of semantics to dispute naive
>> generalizations?
>> I for one would find it really neat if we had such a list of examples
>> on-line for use in courses at all levels and program officers at
>> funding agencies, too.
>> Any other examples than the one above? One is a random hit, two is a 
>> coincidence, three makes a pattern. -- Matthias