[sanxiyn]

No, the rule I stated is what is actually implemented.

Like all type checking technology, the rule is about static behavior, not dynamic behavior. So halting problem is irrelevant.

Rust accepts all programs that follow the rule in static behavior. It's not a subset, and it's not a best effort to prove. It's the complete statement.

"Access" means source code construct to read or write. Rust doesn't care whether the construct is actually executed in runtime.

[estebank]

I believe the "subset of correct code" refers to things like the current non-support for things like

    let (left, right) = (&mut foo[..split], &mut foo[split..]);

where you have to rely on things like foo.split_at_mut(split), which are implemented as unsafe under the cover.

I see these are limitations but not show-stoppers in any way.

[ajross]

It's surely not a showstopper when it's on one line, but again the problem in practice is that those slices may be other operations or hidden behind other APIs, and happening at different depths in a complicated call tree, and you get an error only up at the top when what you're doing looks "clearly correct".

Yes, sure, the rule in question may be simple in the abstract (it's a compiler, after all -- they're just software doing straightforward things). But the ability for the poor programmer to detect which rule is being violated where is a lot more limited than the compiler is designed for. Thus the user with the upthread complaint, which is hardly unique.

I mean, at the end of the day if Rust wants to be an everyday language for this kind of everyday problem, the analysis paradigm needs to be communicated much better to everyday hackers (via docs, error messages, whatever). When Rust was new this seemed like just a technical problem to be solved with software maturity. I guess at this point after several years of regularly returning to play with Rust and being frustrated every time, I've mostly given up.

[sanxiyn]

Sure, but you claimed there is no simple formal rule. That's simply false. It's just that the formal statement is not front and center in documentations, because it is not very useful to learn the rule, and most documentations are targeted to learners.

[sanxiyn]

Yes, but the rule is still complete. What is going on is "place" is currently defined to be local x, or field x.f, or index x[i], but all x[i] are merged to x[*]. Rust's so-called NLL changed definition of "live". The point is, the rule is simple, formal, and complete. It is neither an ad hoc rule nor a best effort prover.

[ajross]

> What is going on is "place" is currently defined to be

Not to belabor this growing thread, but here's the disconnect. I complained the rules were ad hoc and complicated, you replied that they were simple, and when challenged on an edge case your treatment is to add another clause to re-define a term you used in isolation earlier.

That's what "ad hoc and complicated" means.

[sanxiyn]

"place" and "live" have their respective intuitive definitions. To clarify, "place" is a set of bytes in the memory. "live" means it is used again. But both are runtime concepts, so Rust compiler needs to compute static approximation of these runtime concepts. This static approximation is what is complex and changing. But the principle is simple.

Actually, my elaboration of "place", local/field/index, is nearly complete. The only thing missing is upvar, which is local captured in closure. Pre-NLL "live" is simple: expression is live from the definition to the end of the containing statement, and declaration is live from the definition to the end of the containing block. Post-NLL "live" is connected region of control flow graph from the definition to potentially multiple last uses. Really, that is the whole story.

There are two changes currently in development. One changes definition of "place" to include field captured in closure, in addition to local captured in closure. The other is more drastic, changing definition of "live": a loan is live where the loan is origin of a variable and the variable is live. This is great, because current approximation is equivalent to union of all origins.

[ajross]

Link to the relevant spec then? Admittedly my intuition is a year stale at the moment, but I went looking hard for this at one point and found nothing other than source code.

[sanxiyn]

No spec, because technical details are complex, but spec, when it is written, will just be an elaboration of "It is an error to access a place, when an access conflicts with a loan, and the loan is live". This has never changed since Rust 1.0, more than 5 years. Spec will just need to define "place" and "live" and that takes time.

[iudqnolq]

There's no spec yet, but there are working groups working on it.