[bitc-dev] {,de}allocation

[Mark S. Miller]

Jonathan S. Shapiro wrote:
> The control is the proof. Unfortunately, some facts have to come from
> outside the proof.
> 
> Mark: you are seeking a degree of trust that BitC cannot deliver and
> still meet its design objectives. The best answer to what you ask is
> "disallow explicit free". Yes, we can and will provide a means to check
> for that at link time.

If you provide a means to "disallow explicit free" at link time, and you 
continue to control the ability for a module to introduce mutable static state 
or to import modules that do, then, AFAICT, current BitC remains an 
object-capability language that provides the degree of trust I seek. What 
remaining conflict are you worried about?


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


-- 
Text by me above is hereby placed in the public domain

     Cheers,
     --MarkM