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

[Sandro Magi]

David Wagner wrote:
> If anyone knows of any more sophisticated techniques for reasoning about
> resource exhaustion, denial of service, liveness, and progress in
> general-purpose programming languages -- techniques that are actually
> practical for everyday programming tasks -- I would be very interested
> to learn about them.

Linear type systems are used to reason about resource use, ie. when
memory is safe to be freed, not using a file handle after close() was
called on it, etc. Linear types have been combined with regions in a few
papers I've come across, so there is some work being done in this area.
I can't recall any particular paper that attempted to automatically
infer resource bounds though.

I'm less familiar with "uniqueness types" as used in the Clean language,
but they have some association with linear types as well IIRC.

Sandro