[cap-talk] 'Destroy' vs 'Sever'

[Sandro Magi]

Jonathan S. Shapiro wrote:
> Part of the disconnect that I think you and David Hopwood are having
> stems from the fact that in a language-based system the duality of
> storage and (language) object is never exposed in the operations. Indeed
> it *cannot* be, as the hiding of this duality is one of the root sources
> of language safety. This explains in part why malloc cannot be
> implemented within a conventional safe language. Doing so would require
> a combination of monadic style and dynamic cast that has not been
> explored in the safe language realm. Realizing free() in a safe system
> [even in the underlying version called by GC] is even MORE complex --
> probably beyond what type systems are able, in principle, to capture.

Manual memory management is available in sophisticated type systems like
the capability calculus [1]. A slightly more flexible system is [2].
They can even type the interface to the underlying garbage collector,
though [2] purportedly does so more effectively. Most such systems are
prototypes at best though, like Microsoft's Vault language.

Sandro

[1] http://citeseer.ist.psu.edu/28014.html
[2] http://citeseer.ist.psu.edu/638171.html
[3] http://research.microsoft.com/vault/