[bitc-dev] Capture problem with by-ref
Jonathan S. Shapiro
shap at eros-os.com
Thu Mar 13 09:34:53 EDT 2008
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
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.
More information about the bitc-dev