[PRL] the "success" of types

[Felix S Klock II]

Will-

On May 20, 2006, at 6:25 PM, William D Clinger wrote:

> Felix wrote:
>> I'm sorry, what was this point of this example?
>
> That one can indeed "write an invariant that states:  Right now,
> x and y are both lists of some type T (though at other times
> they might not be of the same type)" in Java.
>
>> John said that you can't write down certain time dependent invariants
>> of practical interest.
>
> He was wrong.

Would you agree that in your example, you could have written the same  
invariant down as a comment in English in Java 1.4, and that it would  
have had the same effect (or lack thereof) on the dynamic semantics?

If so, would you agree that is a shift from talking about programming  
language research over to software development methodology?   
(Although maybe we've only been talking about the latter this whole  
time, and I just missed that aspect of the conversation.)

(Or maybe Literate Programming matters and we should start  
investigating that as a PL issue?)

-Felix