4 ms·
The Rust compiler will not solve the halting problem. It is pretty trivial to write programs which are safe if and only if they halt. So 100% safe is simply abs
by Retra 9y ago
The Rust compiler will not solve the halting problem. It is pretty trivial to write programs which are safe if and only if they halt. So 100% safe is simply absurd.
- madez 9y agoThat is trivially obvious, but writing a performant vector implementation is not solving the halting problem. Let me restrict it to the faintly weaker "I hope we don't settle for unsafe being okay forever where we can prove safety".
- andrewflnr 9y agoYou don't need to solve the halting problem just to verify an existing proof of a semantic property, nor to use smarter heuristics to avoid requiring such a proof. 100% safe is totally reachable, though I bet the syntax would be pretty hairy added to today's Rust.
- jononor 9y agoWould need to get rid of C FFI, as that cannot be 'safe' in Rust?
- andrewflnr 9y agoHmm, good point. You'd have to extend the formal verification into the C code, at least. If you can do that, it might be easier to just write verified C.
- Retra 9y agoInline ASM can't be verified either.
- andrewflnr 9y agoInline ASM is exactly as verifiable as the underlying CPU, given an adequate model in the verifier. That's probably easier than verifying C, which introduces extra ambiguity in its semantics. But yeah, verifiable CPUs would be nice.