[bitc-dev] {,de}allocation

[Mark S. Miller]

Mark S. Miller wrote:
> 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.

Other examples of the same principle:

* An unprivileged module could be allowed to introduce secret static mutable 
state, for example, for use as a memoizing cache, if accompanied by a proof 
that this mutability has no overtly observable effects.

* We could allow a non-bounds-checked array store if accompanied by a proof 
that it would be within bounds. (Lacking an integrated proof system, Emily had 
to simply prohibit OCaml's Array.unsafe_set.)

* We could even allow the loading of arbitrary assembly code, if accompanied 
by a proof that all its observable effects were equivalent to an unprivileged 
BitC program that would have been accepted.

Having a proof system integrated into a language does open up interesting new 
degrees of freedom.

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

     Cheers,
     --MarkM