On Oct 4, 2013, at 11:09 AM, "Jonathan S. Shapiro" <[email protected]> wrote:
> 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). You probably know this already, but just in case: the other worry is that rust falls back to runtime checking for some kinds of invariants: http://pcwalton.github.io/blog/2013/01/21/the-new-borrow-check-in-a-nutshell "For @mut boxes, the new borrow checker inserts runtime checks to enforce the pointer rules. Attempting to mutate an @mut box while a pointer to its contents exists results in task failure at runtime, unless the mutation is done through that pointer." Geoffrey
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
