Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

What kind of guarantees does the type system provide? Can I say that no terminating/productive Rust program leaks memory, full stop?


Rust's type system statically guarantees that memory will never be accessed after it is freed, so no segfaults, no use-after-frees, no double-frees, no iterator invalidation, etc. It also statically eliminates data races between concurrent tasks.

In the past Rust has attempted to use the type system to prevent memory leaks in certain cases, but the features that attempted to do so were deemed overly restrictive to use for practical purposes. Nowadays I'm sure it's possible to leak memory if you try. Honestly I've never heard of a Turing-complete language whose type system can provide such a guarantee.


> Honestly I've never heard of a Turing-complete language whose type system can provide such a guarantee.

SPARK (a dialect of Ada) can, I believe. But it does so by forbidding allocation :)


Doesn't it make a stronger guarantee, that you cannot cause an invalid dereference? In addition to what you mentioned, this would also cover bounds-checking, trying to dereference a pointer that was never allocated, etc.

Also does it enforce that memory is consistently used as a single type? Can you allocate a byte array and then cast it to an appropriately sized array of integers?


  > Doesn't it make a stronger guarantee, that you cannot 
  > cause an invalid dereference?
I'm not knowledgeable enough to answer that question precisely.

However, I can tell you that Rust's type system is not strong enough to obviate bounds checking. I hear you'd need something like Idris' dependent types for that. Rust bounds checks arrays dynamically (there are `unsafe` functions available to index an array without bounds checks), and avoids bounds checking on arithmetic by guaranteeing that fixed-sized integers will wrap on overflow (which is gross, but might be changed to fail-on-overflow if it doesn't hurt performance too much).

  > Can you allocate a byte array and then cast it to an 
  > appropriately sized array of integers?
You can't do this in safe code, but you can in `unsafe` code via the `std::cast::transmute` function, which does still enforce that both types are the same size.


> However, I can tell you that Rust's type system is not strong enough to obviate bounds checking.

That's a bummer. It seems doable, but maybe it is too complex.

> avoids bounds checking on arithmetic by guaranteeing that fixed-sized integers will wrap on overflow (which is gross, but might be changed to fail-on-overflow if it doesn't hurt performance too much).

That would be nice as a default, but I'd be afraid it would hurt performance too much for numerical code. You'd definitely want a way to express arithmetic should be allowed to overflow (ie. that omits the check).

On a related note, one thing that is sorely missing in C and C++ is a way to test whether a value will overflow when converted to a different type (I wrote a blog article about this point: http://blog.reverberate.org/2012/12/testing-for-integer-over...)


> That's a bummer. It seems doable, but maybe it is too complex.

In general, eliminating runtime bounds checking is solving the halting problem.

  let v = [1, 2, 3];
  if halts(some_program) { v[1000] } else { v[0] }
Of course, this doesn't meant that it's impossible in a subset of cases, e.g. people are doing work on fast range analysis for LLVM, which would be able to remove some of the bounds checks sometimes: http://code.google.com/p/range-analysis/ (that analysis also applies to the arithmetic, and apparently only makes things single-digit percent slower (3% iirc).)


> In general, eliminating runtime bounds checking is solving the halting problem.

Your example does not convince me that this follows. In cases where the compiler cannot statically prove which branch will be taken, I would expect it to require that either path can be executed without error (so in your example compilation would fail). But you could use static range propagation to allow code like this (given in C++ syntax since I'm a Rust novice):

  void f(int x[], unsigned int n) {
    n = min(len(x), n);
    for (int i = 0; i < n; i++) {
      x[i];
    }
  }
Maybe not the greatest example since I would hope that Rust+LLVM would hoist its internal bounds-check to emit something very much like the above anyway. I guess intuitively I just hope that there's more that can be done when it comes to static bounds-checking.


Well, if you throw the halting problem at it then all of your static analysis goes away since you can use general recursion to write arbitrarily typed expressions. That's why things like Idris have termination checkers.


Yeah, there's definitely some fuzziness around the edges here since general recursion can break invariants in hard to detect ways.


You can't even say that about languages _with_ a GC. At least not as long as you use the practical definition of "leaks memory", which is that the memory remains alive until the application shuts down. Here's a simple example of a memory leak in JS in that sense (modulo nontrivial manual cleanup, obviously):

  window[Math.random()] = new Array(100000);
A much more interesting question, in some ways, is what guarantees you have about not accessing no-longer-alive objects. That's where Rust has some serious advantages over C++, say.


I think you could in raw linear logic—you wouldn't be allowed to introduce a type unless you eliminated it later.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: