3 ms·
> It relies on you trusting code that (supposedly) expert programmers have written, and which has been reviewed hundreds of times. Which is no better than C. T
by Manishearth 11y ago
> It relies on you trusting code that (supposedly) expert programmers have written, and which has been reviewed hundreds of times. Which is no better than C.
This is a vast oversimplification.
It relies on you trusting tiny bits of unsafe code which have been carefully reviewed. This is opposed to entire C codebases which need reviewing. It's much, much easier to audit 10 lines of unsafe code than it is to audit an entire application.
The vast majority of Rust code is not unsafe.
- tomp 11y agoExactly. Just as I've written in my post: > Rust is still a huge improvement > Except that it's not guaranteed
- Manishearth 11y agoYou will never be able to get both 100% guaranteed memory safety and low level control/performance. Opposing it based on principle means that you'll never move on to anything better because a perfect solution doesn't exist. For what it's worth, you can write quite a lot in 100% safe code, such that you have to trust only the standard library. Which is the case for any programming language. So, the argument on the front page is true. It does guarantee memory safety in safe Rust code, as much as possible. It gives you the tools to extend your abstractions with unsafe Rust code, which you need to supply your own guarantees with.
- kazagistar 11y ago> You will never be able to get both 100% guaranteed memory safety and low level control/performance. Sure you can. You just need a full fledged proof engine instead of "merely" a type system.
- Manishearth 11y agoWell, ok. I guess that's too heavyweight, though. However, http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
- scott_s 11y agoSince tomp objects to trusting code, then I agree with Manishearth: if you're never willing to trust code, then you can never have guarantees. Even the proof engine is trusted code.
- tomp 11y agoWell, you have to trust something... Silicone manufacturer, CPU designer, the OS, the compiler... But the big difference is, if I can do proofs and the compiler breaks my trust, that's a bug in the compiler. On the orher hand, Rust disallows complex proofs entirely, so I have to use unsafe code and trust random humans!
- Rusky 11y agoThe compiler is just as much written by random humans as anything else.
- elcritch 11y agoThis. 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.