Bos: Do we need a "Rust Standard"?

Posted Oct 28, 2022 11:09 UTC (Fri) by Karellen (subscriber, #67644)
In reply to: Bos: Do we need a "Rust Standard"? by tialaramex
Parent article: Bos: Do we need a "Rust Standard"?

it's a semantic constraint on a computation and so Rice's theorem says it's Undecidable.

Surely it's only undecidable for it to determine whether any arbitrary program either definitely satisfies the constraint, or definitely does not.

But that's not what Rust's borrow checker needs to do. Rust's borrow checker only needs to determine that a subset of programs definitely satisfy the constraint. If it cannot prove that an arbitrary program can satisfy the constraint, it can reject it. It doesn't matter if the reason the program cannot be proven to satisfy the constraint is because it does not, or because the checker is not powerful enough, or because that program is actually an undecidable case.

If the checker, rigorously implemented to the spec, can prove that an acceptably useful subset of valid programs pass it, it (and, by extension, Rust) are valuable additions to our programming language toolbox.