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
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
