[cap-talk] 'Destroy' vs 'Sever'
smagi at higherlogics.com
Tue Nov 27 18:40:39 EST 2007
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 . A slightly more flexible system is .
They can even type the interface to the underlying garbage collector,
though  purportedly does so more effectively. Most such systems are
prototypes at best though, like Microsoft's Vault language.
More information about the cap-talk