RefCell, why borrowing is checked only in runtime

Hypothetically, if the compiler could prove at compile time that RefCell followed the borrowing rules, then using RefCell would be precisely equivalent to using a plain reference, and thus RefCell would be redundant and serve no purpose.

RefCell is for those times it is NOT provable. No matter how good you make the compiler, there will exist code that you can not prove the behavior of. see: the halting problem.

Sure, the compiler can be improved to prove compliance in more situations, but never ALL situations.

9 Likes

See my qcell crate which does extend compile-time borrow checking into cell types, using three different techniques. However the restrictions will only suit certain uses. This can successfully replace uses of RefCell in some places, though. I use it in my Stakker actor runtime to prove at compile-time that no actor instance method can access the state of any other actor instance.

Personally I see RefCell as a panic waiting to happen, so I prefer to avoid it wherever possible. Probably once you understand how the qcell crate cell types work, you'll better understand the limitations of compile-time borrow checking of cell types, at least what's possible in the Rust borrowing model.

6 Likes

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.