On Thu, 2008-03-13 at 02:11 +0000, David-Sarah Hopwood wrote: > A linear type system is potentially capable of ensuring that a mutable > reference can be passed into prepare(...), but that no aliases derived > from that reference remain after prepare has returned.
Yes. And there are other reasons to be interested in linear type systems as well. But at some point we have to strike a balance between cleverness and utility. In spite of the fact that the work started at a Research University, BitC was not intended to be a vehicle for research into programming languages and type systems. It was intended to be on the on hand a pragmatic tool and on the other a vehicle for software verification and checking research. So at this point I'm in the mode of removing or restricting anything that gets in the way of near-term practical use. > I'm trying to get a handle on precisely which problem(s) you are > concerned about with respect to auditability -- is it the potential > for aliasing of a reference after the procedure to which it was passed > has returned? I'm actually not all that worried about the audit problem. That said, the answer to your question is elusive because the audit goal is pretty subjective. The end goal is for a (human) auditor to be able to examine code and (a) feel comfortable that they understand what is going on well enough to evaluate it, and (b) be technically justified in feeling that comfort. There is no particular set of technical features and restrictions that can satisfy this, though there are some that clearly rule it out. It's a subjective and somewhat slippery thing to try to get at. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
