3 ms·
If you're trying to analyse a program statically and find some property of its runtime behaviour, the halting problem only gets in the way when you need to be a
by mjw1007 7y ago
If you're trying to analyse a program statically and find some property of its runtime behaviour, the halting problem only gets in the way when you need to be accurate about both whether the runtime behaviour does or doesn't have the property.
Here, it's OK if the borrow checker rejects some programs which the stacked-borrows runtime model would say don't in fact invoke undefined behaviour, so long as it doesn't accept any which do.
(And it surely will give some rejections of that sort, for example if I violate the borrowing rules in a function which is never called.)
- kd5bjo 7y agoAlso, this is the primary reason that unsafe exists— there exists code that is both useful and correct but the borrow checker can’t properly verify. It’s a marker that tells the compiler it’s not responsible for verifying that code.
- smaddox 7y agoTo clarify, the borrow checker is not disabled in unsafe blocks. Unsafe blocks just allow raw pointer dereferencing, which can be used to bypass the borrow checker.