Jonathan S. Shapiro wrote: > The "free" keyword is reserved, but allowing it to be invoked without > discharge creates safety issues. Having said that, I should admit a > sleazy hidden fact: the prover will need DEFAXIOM to allow programmers > to introduce facts that cannot be proved. In particular, DEFAXIOM is > needed to describe the behavior of assembly support routines. So free > can be used badly if desired.
Could the use of unsafe-free be controlled, in much the way that BitC currently controls the ability to introduce mutable static state? If not, then a malicious library writer can use unsafe-free to violate memory safety. > Haskell, so far as I know, does not have free. AFAIK too, that's correct. But Haskell does have a primitive, unsafePerformIO, that allows code to violate declared constraints on side effects. AFAIK, in Haskell currently, the ability to use unsafePerformIO to escape this checking in uncontrolled. Were someone to do an Emily-like[1] taming of Haskell, to derive a corresponding object-capability language, I would advocate that they make the ability to unsafePerformIO into a controllable permission that is denied by default. For BitC, could unsafe-free (or perhaps even DEFAXIOM) be similarly controlled? 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 -- 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
