Sure, there's a reason I said "Extremely difficult" not "Impossible". Defying Rice without losing generality is mathematically impossible. This is on that cont

Sure, there's a reason I said "Extremely difficult" not "Impossible". Defying Rice without losing generality is mathematically impossible. This is on that continuum where it's definitely neither impossible nor easy enough that we can just let some bored grad student knock out the answer, and so now somebody who wants this must do lots of hard work. I think a specification which says e.g. here's the semantic requirement, here's a rule for scoped borrows which works, you must do at least that, but you can do more however you must not allow anything which violates the semantic requirement - would be great, but if you had that rule in your standard then people can write conforming Rust programs which don't compile - they need a yet-to-be-written smarter compiler to figure out why they're legal, which is kinda annoying as a language feature.