[PRL] the "success" of types

[John Clements]

On May 20, 2006, at 3:25 PM, William D Clinger wrote:
>
>> John said that you can't write down certain time dependent invariants
>> of practical interest.
>
> He was wrong.
>
>> I inferred that he wanted this invariant to
>> be automatically checked (statically, I assume, though some may be
>> happy with a dynamic check, as long as it happens at a sensible
>> place).
>
> You are probably right about what John wanted and should have
> said, but what John actually claimed is that he "can't write"
> an invariant...".  In my very first post of this thread, I wrote:
>
>     First of all, checking of invariants is not at all the same thing
>     as thinking about them or writing them down.
>
> I seized upon John's false claim as an opportunity to make this
> point yet again.

I want to thank Will for pointing out my mistake, and Felix for  
clarifying the point.


Thanks!

John Clements

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2484 bytes
Desc: not available
Url : https://lists.ccs.neu.edu/pipermail/prl/attachments/20060521/2cb2956f/smime.bin