News for hackers. Stuff that matters.

A comment on The Rustonomicon: The Dark Arts of Advanced and Unsafe Rust Programming. Parent comment

Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru... by foota on Sunday July 10, 2016 @04:36PM (#12067155)
I don't know much about what I'm about to say, but I've always thought it would be cool to embed some proof language like coq inside the rust compiler so that devs can write proofs that their unsafe code obeys some properties that the rust compiler can use.
[ Parent | on HN ]
Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru... by __s on Sunday July 10, 2016 @08:19PM (#12067960)
Wouldn't it be better to skip writing the unsafe code, & have the proof generate proven-safe unsafe rust code?
[ Parent | on HN ]
Re:The Rustonomicon: The Dark Arts of Advanced and Unsafe Ru... by foota on Sunday July 10, 2016 @09:23PM (#12068275)
Aw, see, this is me showing what I don't know :) I was thinking it would be something similar to this: https://en.wikipedia.org/wiki/Proof-carrying_code except at compile time.
[ Parent | on HN ]