5 ms·

> But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs? Empirically, program

> But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs? Empirically, programs written in memory-safe languages produce multiple orders of magnitude fewer memory-related bugs than C and C++ codebases do. > Centralizing the memory management code to some well tested core---like the Rust compiler or some C lib That isn't practical in C (or in C++). "Memory management" here means "pointers", and you can't program in C or C++ without pointers.

wahern 9y ago
How many buffer overflows were involved in the Equifax leak? The ultimate solution to the problem is formal verification. Rust solves this for buffer overflows, but nothing else. It's a one trick pony. Someone posted this interesting nugget on HN the other day: https://www.youtube.com/watch?v=zt0OQb1DBko Aside from some of the awkward ergonomics, its mechanism for formal specification looks brilliant. And you get to keep C's bag-of-bytes object manipulation and pointer arithmetic (when you want it) without having to resort to unsafe{}. For projects where it's worth the effort to carefully declare precise typing semantics (because safety, performance, whatever), I want a wholistic solution. Otherwise my time and money is better spent throwing Javascript or Python at the problem, which solve the buffer overflow problem just as well.
- pcwalton 9y ago
  > Rust solves this for buffer overflows, but nothing else. It's a one trick pony. Completely false. Rust's design prevents all memory safety problems (that's what "memory safe" means). Buffer overflows aren't even the most pernicious kinds of memory safety problems anymore. Use after free is worse, and Rust spends most of its complexity budget on preventing that.
  - wahern 9y ago
    I spoke poorly. My point was that memory safety is but _one_ issue of a far larger problem. And Rust indeed solves it, or at least Rust provides an ergonomic environment for writing solutions that are memory safe. Which is different than saying it's easy to do this in an absolute sense. But certainly writing a program in Rust without using unsafe{} at all is still easier and more ergonomic than using other systems (e.g. annotation based frameworks which weren't baked into the language from inception) for equivalently safe behavior. But if you watch the video, the presenter makes a great point: Rust's borrow checker is an amazing piece of technology, but it's inaccessible to the programmer. It's an implementation detail used to provide proofs for a narrow constraint--memory safety. Imagine if Rust provided syntax and semantics which not only allowed you to effectively implement the borrow checker yourself using a more general declaration system, but implement any other kind of formal specification needed to prove the higher-level semantics of your code. In other words, imagine if a more general formal specification system were as first-class as the ownership- and mutability-oriented syntax are in Rust; a language that unifies the annotation model of solutions like Ada SPARK and Frama-C, but which is properly integrated into the language. And that's what ATS is exploring. As the presenter says, ATS might be ugly as a systems language (because misallocated complexity--some easy things are too complex, some complex things are too easy--increases cognitive load and reduces efficiency), but its mechanism for formal specification is brilliant. Improve ATS, or apply it's novel approach to a language designed as a daily driver, and you'd finally have a realistic answer to the plague of buggy infrastructure software. I realize this sounds like I'm making perfect the enemy of the good here. But I stand by my point: major failures like Equifax rarely involve memory safety, per se. Arithmetic issues are far more common, and even those are on the long tail of a much larger issue; namely, an inability to [efficiently] provide verifiable specifications for higher-level semantics. We hyper focus on buffer overflows, arithmetic overflows, etc, because we understand them and we know (at least in principal) how to fix them. But those are psychological blinders that cause us to miscalculate relative risks. We tend to overestimate the cost of problems we can fix relative to the cost of problems we're unsure about how to fix.
    - roca 9y ago
      Full verification is extremely expensive, not just to create the proofs, but also to maintain them as the software evolves. Telling C programmers to go directly to full verification is, indeed, making the perfect the enemy of the good. And you are missing an important point here. Once you have a reasonably sound and rich type system, you can leverage the type system in library API design to eliminate classes of higher-level bugs. For example, Rust crypto libraries can leverage Rust's affine type system to ensure you don't use a nonce more than once. The Apache Struts vulnerability was about failing to distinguish trusted vs untrusted input; that distinction can be expressed and checked in type systems.
xelxebar 9y ago
> Empirically, programs written in memory-safe languages produce multiple orders of magnitude fewer memory-related bugs than C and C++ codebases do. This kind of emperically-driven motivation is great! Would you mind pointing me to some sources? My google-fu didn't immediately yield anything helpful.

wahern 9y ago

How many buffer overflows were involved in the Equifax leak? The ultimate solution to the problem is formal verification. Rust solves this for buffer overflows, but nothing else. It's a one trick pony. Someone posted this interesting nugget on HN the other day: https://www.youtube.com/watch?v=zt0OQb1DBko Aside from some of the awkward ergonomics, its mechanism for formal specification looks brilliant. And you get to keep C's bag-of-bytes object manipulation and pointer arithmetic (when you want it) without having to resort to unsafe{}. For projects where it's worth the effort to carefully declare precise typing semantics (because safety, performance, whatever), I want a wholistic solution. Otherwise my time and money is better spent throwing Javascript or Python at the problem, which solve the buffer overflow problem just as well.

pcwalton 9y ago
> Rust solves this for buffer overflows, but nothing else. It's a one trick pony. Completely false. Rust's design prevents all memory safety problems (that's what "memory safe" means). Buffer overflows aren't even the most pernicious kinds of memory safety problems anymore. Use after free is worse, and Rust spends most of its complexity budget on preventing that.
- wahern 9y ago
  I spoke poorly. My point was that memory safety is but _one_ issue of a far larger problem. And Rust indeed solves it, or at least Rust provides an ergonomic environment for writing solutions that are memory safe. Which is different than saying it's easy to do this in an absolute sense. But certainly writing a program in Rust without using unsafe{} at all is still easier and more ergonomic than using other systems (e.g. annotation based frameworks which weren't baked into the language from inception) for equivalently safe behavior. But if you watch the video, the presenter makes a great point: Rust's borrow checker is an amazing piece of technology, but it's inaccessible to the programmer. It's an implementation detail used to provide proofs for a narrow constraint--memory safety. Imagine if Rust provided syntax and semantics which not only allowed you to effectively implement the borrow checker yourself using a more general declaration system, but implement any other kind of formal specification needed to prove the higher-level semantics of your code. In other words, imagine if a more general formal specification system were as first-class as the ownership- and mutability-oriented syntax are in Rust; a language that unifies the annotation model of solutions like Ada SPARK and Frama-C, but which is properly integrated into the language. And that's what ATS is exploring. As the presenter says, ATS might be ugly as a systems language (because misallocated complexity--some easy things are too complex, some complex things are too easy--increases cognitive load and reduces efficiency), but its mechanism for formal specification is brilliant. Improve ATS, or apply it's novel approach to a language designed as a daily driver, and you'd finally have a realistic answer to the plague of buggy infrastructure software. I realize this sounds like I'm making perfect the enemy of the good here. But I stand by my point: major failures like Equifax rarely involve memory safety, per se. Arithmetic issues are far more common, and even those are on the long tail of a much larger issue; namely, an inability to [efficiently] provide verifiable specifications for higher-level semantics. We hyper focus on buffer overflows, arithmetic overflows, etc, because we understand them and we know (at least in principal) how to fix them. But those are psychological blinders that cause us to miscalculate relative risks. We tend to overestimate the cost of problems we can fix relative to the cost of problems we're unsure about how to fix.
  - roca 9y ago
    Full verification is extremely expensive, not just to create the proofs, but also to maintain them as the software evolves. Telling C programmers to go directly to full verification is, indeed, making the perfect the enemy of the good. And you are missing an important point here. Once you have a reasonably sound and rich type system, you can leverage the type system in library API design to eliminate classes of higher-level bugs. For example, Rust crypto libraries can leverage Rust's affine type system to ensure you don't use a nonce more than once. The Apache Struts vulnerability was about failing to distinguish trusted vs untrusted input; that distinction can be expressed and checked in type systems.

xelxebar 9y ago

> Empirically, programs written in memory-safe languages produce multiple orders of magnitude fewer memory-related bugs than C and C++ codebases do. This kind of emperically-driven motivation is great! Would you mind pointing me to some sources? My google-fu didn't immediately yield anything helpful.