> Has the third been done, or is someone working on it?
Can this be done though? The way I understand this: Either 1. the whole model is specified and can be proven, (which wouldn't need the second step) or 2. you can only find specific counter-examples, not demonstrate there aren't any. (That would be like a solution to the halting problem) Did I miss something?
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.)
Also, 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.
To 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.
Can this be done though? The way I understand this: Either 1. the whole model is specified and can be proven, (which wouldn't need the second step) or 2. you can only find specific counter-examples, not demonstrate there aren't any. (That would be like a solution to the halting problem) Did I miss something?