Exploring Rust (from C#)

Re:Exploring Rust (from C#) by elcritch on Wednesday March 23, 2016 @05:57PM (#11348599)

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!

[ Parent | on HN ]

Re:Exploring Rust (from C#) by Manishearth on Wednesday March 23, 2016 @09:23PM (#11349868)

This is already being worked on http://plv.mpi-sws.org/rustbelt/

[ Parent | on HN ]

Re:Exploring Rust (from C#) by elcritch on Sunday March 27, 2016 @03:33PM (#11371162)

Fantastic! 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.

[ Parent | on HN ]