3 ms·
Rice's theorem isn't relevant here. The goal is not to create a system that produces no false positives, it's perfectly fine to do a conservative syntactic anal
by kibwen 2y ago
Rice's theorem isn't relevant here. The goal is not to create a system that produces no false positives, it's perfectly fine to do a conservative syntactic analysis that allows false positives but disallows false negatives, and it's then possible to produce a formal proof that this analysis is sound. It is this formal proof that I would expect to be included in a specification in lieu of English prose.
- tialaramex 2y agoSure, 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.