5 ms·

I'm always confused by the "safe language" evangelism. Reducing cognitive load is a Good Thing TM; I get that. But aren't we just trusting the Rust compiler and

I'm always confused by the "safe language" evangelism. Reducing cognitive load is a Good Thing TM; I get that. But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs? Centralizing the memory management code to some well tested core---like the Rust compiler or some C lib---sounds to be the crux of wiring memory safe code, not the language.

bjz_ 9y ago
Trouble is that in C there is no way to encapsulate the unsafe code. Rust has tools that let you do that - it's not perfect, but depending on the level you are working at you can even build operating systems like Redox with the majority of the code in safe Rust. The language has not been formally specified which is a concern, but this is an active area that is also being worked on in collaboration with universities. This should make it easier to write unsafe code in combination with theorem provers like Lean or Coq for even greater confidence, and ensure that any soundess holes in the type system are found.
- blub 9y ago
  The ability to grep for "unsafe" is probably the biggest advantage of Rust. I would love to have that in C++.
sanxiyn 9y ago
You are right. On the other hand, in practice, implementing it in language (really, compiler) seems more effective than in library, as in reducing number of bugs. Why it is so is an interesting question, but is not very relevant to empirical basis of safe language evangelism.
chrismorgan 9y ago
Concerning Rust specifically—Rust’s memory safety comes from its type system; specifically, its strong ownership model, which leads to its lifetime model. Without these, you simply can’t have a fast, memory-safe language: either you surrender speed, by boxing everything, or you surrender safety. My point is that it’s not possible to just isolate the hazardous chunks into a well-tested core; it needs to be pervasive in the language’s memory model and type system in a way that C and C++ just don’t have.
- wahern 9y ago
  > Without these, you simply can’t have a fast, > memory-safe language: either you surrender > speed, by boxing everything, or you surrender safety. Not only can you have speed and safety without Rust's rigid enforcement of exclusive ownership, you can do even better--even faster and with even stronger security guarantees: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko http://www.ats-lang.org/ http://www.ats-lang.org/
weberc2 9y ago
Seems like it would be easier to audit and/or prove a compiler than all of the important software built from it.
pcwalton 9y ago
> 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.

bjz_ 9y ago

Trouble is that in C there is no way to encapsulate the unsafe code. Rust has tools that let you do that - it's not perfect, but depending on the level you are working at you can even build operating systems like Redox with the majority of the code in safe Rust. The language has not been formally specified which is a concern, but this is an active area that is also being worked on in collaboration with universities. This should make it easier to write unsafe code in combination with theorem provers like Lean or Coq for even greater confidence, and ensure that any soundess holes in the type system are found.

blub 9y ago
The ability to grep for "unsafe" is probably the biggest advantage of Rust. I would love to have that in C++.

sanxiyn 9y ago

You are right. On the other hand, in practice, implementing it in language (really, compiler) seems more effective than in library, as in reducing number of bugs. Why it is so is an interesting question, but is not very relevant to empirical basis of safe language evangelism.

chrismorgan 9y ago

Concerning Rust specifically—Rust’s memory safety comes from its type system; specifically, its strong ownership model, which leads to its lifetime model. Without these, you simply can’t have a fast, memory-safe language: either you surrender speed, by boxing everything, or you surrender safety. My point is that it’s not possible to just isolate the hazardous chunks into a well-tested core; it needs to be pervasive in the language’s memory model and type system in a way that C and C++ just don’t have.

wahern 9y ago
> Without these, you simply can’t have a fast, > memory-safe language: either you surrender > speed, by boxing everything, or you surrender safety. Not only can you have speed and safety without Rust's rigid enforcement of exclusive ownership, you can do even better--even faster and with even stronger security guarantees: https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko http://www.ats-lang.org/ http://www.ats-lang.org/

weberc2 9y ago

Seems like it would be easier to audit and/or prove a compiler than all of the important software built from it.

pcwalton 9y ago

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