Comment by afdbcreid
3 days ago
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.
3 days ago
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.
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).