←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 3 comments | | HN request time: 0.611s | 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 #
0x000xca0xfe ◴[] No.44512597[source]
As I understand it the borrow checker only has false negatives but no false positives, correct?

Maybe a dumb question but couldn't you just run multiple implementations in parallel threads and whichever finishes first with a positive result wins?

replies(2): >>44512965 #>>44517616 #
1. vlovich123 ◴[] No.44512965[source]
This presumes that checking composes which may not if you have orthogonal checker implementations. You might end up risking accepting an invalid program because part of it is valid under one checker, part under another, but the combination isn't actually valid. But maybe that's not actually possible in practice.
replies(1): >>44515079 #
2. afdbcreid ◴[] No.44515079[source]
Borrow checking is function-local, so if the opsem model is the same and you run the different checkers per-function, there is no such risk.
replies(1): >>44517102 #
3. vlovich123 ◴[] No.44517102[source]
I’ll take your word for that although it feels like there may be other cases. Even still there is the subtle problem that bugs in the proof checkers now result in O(n^m) safety issues because an incorrectly accepted program is more likely to get through 1 of the borrow checkers (similar to how in a distributed system adding single points of failure results in exponentially decreasing reliability).