4 ms·

> 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 i

> 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 ago
Well, ok. I guess that's too heavyweight, though. However, http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
scott_s 11y ago
Since 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 ago
  Well, 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 ago
    The compiler is just as much written by random humans as anything else.
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 ago
  This is already being worked on http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
  - elcritch 11y ago
    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.

> 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 ago

Well, ok. I guess that's too heavyweight, though. However, http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/

scott_s 11y ago

Since 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 ago
Well, 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 ago
  The compiler is just as much written by random humans as anything else.

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 ago
This is already being worked on http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
- elcritch 11y ago
  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.