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

[Sandro Magi]

Jonathan S. Shapiro wrote:
> I *definitely* was not proposing any pointer increment operation that
> would permit a pointer to be used to iterate over a vector! Unless you
> have fat pointers in the style of Popcorn/Cyclone, that is simply
> unsafe.
> 
> In the *presence* of fat pointers, though, I suspect that dependent type
> analysis may be able to deal with the issue in real programs, and more
> importantly provides enough information to explain to the programmer
> what has happened when the analysis fails.

Fat pointers are not necessary if you have a sufficiently powerful type
system. See "Applied Type System with Stateful Views" [1] for an example
of a dependently typed language that supports full pointer arithmetic. A
brief overview is on ATS's homepage [2].

Abstract interpretation might also be able to enforce correct pointer
use, but I've just started in this literature, so I'm not 100% certain
of this.

Sandro

[1] http://citeseer.ist.psu.edu/744971.html
[2] http://www.cs.bu.edu/~hwxi/ATS/ATS.html