3 ms·
This. There's no reason the smaller bits of `unsafe` code couldn't be verified with a proof system (ala COQ). Very few systems can be completely `true` in a mat
by elcritch 11y ago
This. There's no reason the smaller bits of `unsafe` code couldn't be verified with a proof system (ala COQ). Very few systems can be completely `true` in a mathematical sense, including math itself. IMHO, this is a self-defeating argument. E.g. a form of: "math isn't provable so math sucks!".
In the long run, this viewpoint would prevent moving to a system with 5% unsafe/95% safe which could be much more readily proofed using COQ since only a handful of unsafe code needs to be analyzed – I'm assuming proofing code has exponential complexity growth. So basically give Rust 10 years and I bet someone could build a verified stdlib & compiler for Rust!
- Manishearth 11y agoThis is already being worked on http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
- elcritch 11y agoFantastic! Rust keeps getting better... Didn't realize Max Planck institute had a software division. Are you familiar with the state of their progress? I've been wondering when/how people might start applying monads to analyze shared imperative state. It appears to be somewhat of the approach in `Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning` paper listed. Going to have to keep an eye on these folks.