4 ms·
Would need to get rid of C FFI, as that cannot be 'safe' in Rust?
by jononor 9y ago
Would 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.