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

[Jonathan S. Shapiro]

On Mon, 2007-01-01 at 19:24 -0500, Sandro Magi wrote:
> Jonathan S. Shapiro wrote:
> > 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].

ATS is an example of a dependent type system, but it does not eliminate
the need for fat pointers. If the ATS type system passes your program,
you don't have any vector bound errors. However, there are dynamically
correct programs that ATS cannot statically check.

Depending on your goals, these programs either require fat pointers with
run time checks or they require rewriting. Fat pointers are appropriate
if you can tolerate a run time exception (*you* may know that it isn't
thrown, but the compiler does not). Revisions to the program are
indicated if run time exceptions are completely unacceptable, as is true
in many critical control applications.

> 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.

Yes. Recently Paritosh Shroff Hopkins has developed a set of techniques
that he calls "Near-Concrete Program Interpretatoin" that do an
exceptionally good job on this stuff. You can find a link from Pari's
web page at:

  http://www.cs.jhu.edu/~pari/

shap