←back to thread

Tree Borrows

(plf.inf.ethz.ch)
565 points zdw | 3 comments | 09 Jul 25 14:40 UTC | HN request time: 0.611s | source
Show context
fuhsnn ◴[09 Jul 25 16:35 UTC] 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 ◴[09 Jul 25 17:19 UTC] 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 ◴[09 Jul 25 17:53 UTC] 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 ◴[09 Jul 25 21:52 UTC] 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 ◴[10 Jul 25 04:15 UTC] 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).