3 ms·
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 d
by foota 10y ago
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.
- __s 10y agoWouldn't it be better to skip writing the unsafe code, & have the proof generate proven-safe unsafe rust code?
- foota 10y agoAw, 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 https://en.wikipedia.org/wiki/Proof-carrying_code except at compile time.