←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 3 comments | | HN request time: 0.001s | source
Show context
fuhsnn ◴[] No.44512042[source]
I wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics (compile speed, runtime speed, algorithm flexibility, etc.) that projects can choose from.
replies(9): >>44512293 #>>44512361 #>>44512426 #>>44512597 #>>44512841 #>>44513554 #>>44513949 #>>44516880 #>>44516995 #
Ericson2314 ◴[] No.44513949[source]
What you actually want is the underlying separation logic, so you can precisely specify function preconditions and prove mid-function conditions, and the the optomizer can take all those "lemmas" and go hog-wiled, right up to but not past what is allowed by the explicitly stated invariants.

"Rust", in this context, is "merely" "the usual invariants that people want" and "a suite of optimizations that assume those usual invariants, but not more or less".

replies(1): >>44517572 #
1. creata ◴[] No.44517572[source]
Can you help me understand your comment with a simple example? Take slice::split_at and slice::split_at_mut:

    fn split_at(&self, mid: usize) -> (&[T], &[T])
    fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T])
What might their triples look like in separation logic?
replies(2): >>44518278 #>>44523002 #
2. ralfj ◴[] No.44518278[source]
The long answer to this question can be found in https://research.ralfj.de/thesis.html. :)
3. Ericson2314 ◴[] No.44523002[source]
See Ralf's answer but let me give you a bit of extra flavor:

These functions do not memory accesses, they are both from an operational perspective essentially:

p, n -> (p, p + n)

The separation logics I've seen have all have what we might call a strong extensional calculi / shallow DSL embedding flavor. What that means is roughly that there is strong distinction between the "internal" program under scrutiny, and fairly arbitrary external reasoning about it.

I bring this up in order to say that we're very far from "what is the principal type of this expression?" type questions. There are many, many, ways one might type split_at/_mut depending on what the context requires. The interesting thing about these in Rust is really not the functions themselves, but & and &mut. Those types are stand-ins for some family of those myriad potential contexts, in the way that interfaces are always reifications of the possibilities of what the component on the other side of the interface might be.

In the "menagerie of separation logics" I was originally thinking of, there may not be singular & and &mut that work for all purposes. The most reusable form split_at indeed may be tantamount to the simple arithmetic pure function I wrote above, leaving to the caller the proof of showing whatever properties it needs are carried over from the original pointer to the new ones. Given the arithmetic relations, and the knowledge that nothing else is happening (related to the famous frame rule), the caller should be able to do this.