Re: Rather, DSSLs increase modularity, productivity

[Matthias Felleisen <address@hidden>]

On Monday, November 24, 2003, at 04:54 PM, Pascal Costanza wrote:

>
> On 17 Nov 2003, at 20:39, Matthias Felleisen wrote:
>
>> Even though you can write byte code and modify it with a class loader
>> you still have to get it by the byte-code verifier. So, yes, you're 
>> correct
>> a type-soundness result for Java at the source level looks 
>> irrelevant. But
>> the question you really have to pose is how the type soundness for the
>> Java type system relates to the soundness of the byte code verifier. 
>> As
>> far as we know, the second result may imply the first one.
>>
>> I don't know whether anyone has looked into this connection. I'd 
>> expect
>> so given the cottage industry on Java theory results.
>
> The term you are looking for is "binary compatibility". It describes 
> in what ways Java class files may change from release to release so 
> that they don't break dependent programs.
>
> Some of the issues are described in papers about JMangler. See 
> http://javalab.iai.uni-bonn.de/research/jmangler/
>
> I think Sophia Drossopoulou, and probably also others, are working on 
> a formalization of the notion of binary compatibility.

Nope, that's not the term you need.

To get type soundness for a language, you must prove a connection 
between
its source level and the enforcement of the language's contract at 
run-time.
If you can't rely on the latter, your type soundness theorem is bogus.

Example: If ML were to ignore array indexing and just return the bits 
that
any index offset provides, you'd be in deep trouble. So array index 
checking
(either proven away at compile time or most often checked at run-time) 
is
crucial to make type soundness hold up.

This is also true for Java. I suspect that in Java the type soundness
for the source almost doesn't matter at all. The byte code verifier
probably does most of the work, which is why class loaders work at all.

-- Matthias