On Fri, Oct 4, 2013 at 10:02 AM, Florian Weimer <[email protected]> wrote:
> * Jonathan S. Shapiro: > > Then perhaps I misunderstood something. What safety claims are they > > making? > > They intend to provide a safe subset (which is also the default > language) where it's quite unlikely that you bypass memory safety > accidentally. As far as I understand, they won't use formal methods > to ensure that it's impossible, or compile down to an IR which is > fairly certainly memory-safe. It's much stronger than Ada's approach > and safety violations are treated as bugs, but it's likely that they > will keep popping up for a while. Words like "quite unlikely" are cause for concern. This sounds very much like the alleged safe subset is safe only by strong assertion. What worries me here is not that the current implementation is unsafe or buggy - I'm certain that it is, but that's okay. It's still early days. What worries me is that in the absence of formally capturing the type rules (which just isn't that hard), they don't even know if the language is *sound *. In fact, they don't know whether *in principle* a safe implementation is even *possible*. [By "safe" here, I mean for programs that eschew explicitly unsafe constructs.] And it most certainly is *not* stronger than Ada's approach. There is at least a well-defined subset of Ada for which both the type system and the language semantics have been fully formalized: SPARK Ada. Challenge problem: give a set of type rules that show borrowed pointers to be safe. I'm having trouble. Aside: I realized the other day that there is an optimization issue with borrowed pointers: since a borrowed pointer does not represent a "live" reference (for GC), it is imperative that the originating non-borrowed pointer remain live while the borrowed pointers are in use. Here's a very simple sequence that doesn't ensure this (sorry for the made up syntax) extern f(bS: borrowed String); let s = "abcdefg" in f(s); Note that /s/ is not live after the call. In fact, if the architecture specifies that parameters are placed in register %param1, the compiler is completely free here to place /s/ in %param1. This has the effect that if a GC occurs during the call to f(), there are no witnessably live references to that string. It's not difficult to get this right. I point it out to show that borrowed pointers introduce some subtle issues, and it's very easy to get something like this *wrong*. Especially so if your group doesn't have the discipline to write down its invariants (like, say, type rules). shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
