Mark S. Miller wrote:
>>> Any module that has permission to unsafe-free is a central point of failure
>>> for that process as a whole, since the correct function of everything else
>>> in
>>> that process relies on that module to use unsafe-free safely.
>>>
>>> [1] http://www.hpl.hp.com/techreports/2006/HPL-2006-116.html
>> No. Any module that has permission to unsafe-free without a
>> corresponding proof discharge is such a central point of failure.
>
> Please reread the sentence you're quoting. Ignoring your "No." for a moment,
> I
> believe my statement and your reply are in complete agreement. Indeed, they
> seem to be virtually identical. What do you think we're disagreeing about?
Oops, I get it. My mistake. If a module discharges its proof obligation, then,
to my mind, it's just "free"ing, not "unsafe-free"ing. I should have made this
clear.
--
Text by me above is hereby placed in the public domain
Cheers,
--MarkM
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
