[cap-talk] Claim: correct generic wrapping is not possible in principle

[Jonathan S. Shapiro]

On Mon, 2007-01-01 at 02:53 +0000, David Hopwood wrote:
> If values of a parameteric type are only used opaquely (as is very often
> the case for code implementing a generic data structure), then it should
> not be any more difficult to prove the code correct than it would be for a
> specific type. Of course, the resource requirements will depend on the
> instantiating type.

Hmm. I didn't think that through adequately. In particular, I was not
considering procedure arguments. I was thinking in the context of BitC,
which has type classes, and considering things like B-Tree
implementations, where the use of the object is mostly opaque, and the
implementation can be verified as "true contingent on certain properties
being true of the implementations of the type class methods".

-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100