News for hackers. Stuff that matters.

A comment on Why writing a linked list in safe Rust is so damned hard. Parent comment

Re:Why writing a linked list in safe Rust is so damned hard by jononor on Friday February 23, 2018 @05:38AM (#16445483)
Would need to get rid of C FFI, as that cannot be 'safe' in Rust?
[ Parent | on HN ]
Re:Why writing a linked list in safe Rust is so damned hard by andrewflnr on Friday February 23, 2018 @07:15PM (#16450773)
Hmm, 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.
[ Parent | on HN ]
Re:Why writing a linked list in safe Rust is so damned hard by Retra on Friday February 23, 2018 @07:24PM (#16450814)
Inline ASM can't be verified either.
[ Parent | on HN ]
Re:Why writing a linked list in safe Rust is so damned hard by andrewflnr on Friday February 23, 2018 @08:10PM (#16451017)
Inline 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.
[ Parent | on HN ]