Arguably the most important memory safety property, i.e. bounds checking for dynamic arrays, is also not statically checked in Rust.

▲ woodruffw 3 hours ago | parent | next [-]

How would Rust perform static checks on dynamic bounds? That seems like an impossible order, i.e. not a reasonable evaluation criteria for any (general-purpose) language.

(I'm separately skeptical that it's the most important memory safety property; I suspect that a review of Chrome and Firefox 0days would show that UAFs and type confusion are, at least to attackers, equally if not more important.)

▲

zem 3 hours ago | parent | next [-]

ATS could probably do some of this by constructing proofs about the bounds and indices - not in the completely general case of course, but for at least some fraction of what a language without dependent types would have to defer to runtime

▲

ratmice 2 hours ago | parent [-]

those are not dynamic bounds.

▲

LoganDark 2 hours ago | parent [-]

All "dynamic" means is that you don't know or don't prove the precise value statically. However you may know the range of possible values, or you may know properties of your algorithm that mean it can never attempt an out-of-bounds access. Sometimes you don't know any of these things, but sometimes you do.

▲

ratmice an hour ago | parent [-]

What I was (badly) trying to express was more that given static bounds rust could also eliminate dynamic checks. So saying e.g. ATS can eliminate static checks, is kind of switching the target.

	▲	zem 39 minutes ago \| parent [-]
		https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML... is the kind of thing I mean - ATS programs can include proofs that an array access will be safely within bounds, even if we don't have an exact literal subscript in the code.

▲

uecker an hour ago | parent | prev | next [-]

Rust can not do this. But the original claim is that it is all statically checked in Rust, and this is an obvious counter example. Some dependently types languages can prove this statically, also model checking can do this, etc. So it can be done statically as well, but not in Rust.

▲

woodruffw an hour ago | parent [-]

> But the original claim is that it is all statically checked in Rust

Where? The GP's comment says "prefers," which I didn't read to mean a blanket statement. I don't think anybody with more than passing experience in Rust (or C) would make such a claim.

> Some dependently types languages can prove this statically, also model checking can do this, etc. So it can be done statically as well, but not in Rust.

You're couching the part where it can't be done with full generality or can be done with full generality, but with punishing semantics. The appropriate comparison here is with other normal general purpose compiled languages.

	▲	uecker an hour ago \| parent [-]
		I read "Rust prefers to prevent all undefined behavior statically," to also imply that it actually does this, because otherwise the word "all" would not make sense to me in this sentence. Dependently types languages and model checking do exist. They come with tradeoffs, but this is also true for Rust.

▲

LoganDark 3 hours ago | parent | prev [-]

Presumably, they're talking about the possibility of explicitly replacing dynamic bounds checks in cases where it's statically provable that the access will not overrun. That doesn't necessarily mean you lose cases where you genuinely can't prove such a thing, but rather that it would be possible to opt into compiler assistance with proving it, rather than hoping LLVM will have your back. At least, that's how I'd envision such a thing for Rust. This would be similar to how you can already choose whether to invite more of the borrow checker by using references directly, or to do the checks at runtime with Rc/RefCell, etc.

▲

woodruffw 3 hours ago | parent | next [-]

Yeah, that seems like a nice thing that Rust could offer. It strikes me as a weird thing to get hung up on, though, given that the norm in compiled languages - including C - is to express your bounds such that an optimizing compiler can (but won't necessarily) eliminate them.

(You mentioned WUFFS below, which is why I qualified with general-purpose! One thing that WUFFS does that I think Rust could add pretty easily is provable indexing, e.g. allow me to use a `u8` to index a `[u8; 256]` without having to widen to a `usize` first and hope that LLVM optimizes it back out.)

▲

haberman 3 hours ago | parent | prev | next [-]

> rather than hoping LLVM will have your back

My thought here is to proactively verify that LLVM elided the automatic bounds checks in places where you believe that your explicit checks should be sufficient.

That was a key part of my article on "No-Panic Rust": https://blog.reverberate.org/2025/02/03/no-panic-rust.html ("A Dance With The Optimizer")

▲

uecker an hour ago | parent | prev [-]

I merely pointed out that the statement "Rust prefers to prevent all undefined behavior statically" is misleading in the sense that Rust does not do this for all undefined behavior.

▲

LoganDark an hour ago | parent [-]

Maybe if you think of [] as offsetting a pointer rather than calling into an Index (or IndexMut) implementation. Since the return type isn't optional, a panic is the only way to avoid performing an invalid access or manufacturing an unfaithful return value. There are also optional accessors which do not panic, and unsafe/unchecked accessors.

	▲	uecker 38 minutes ago \| parent [-]
		Maybe? I think my statement is clearly correct in the way I formulated it.

▲ wasmperson 2 hours ago | parent | prev | next [-]

This isn't entirely true. Rust's indexing operator performs a dynamic check but the language and stdlib have a number of ways to access array elements without indexing, which is effectively a form of static checking. For example, the following loop is statically guaranteed to not go OOB, and will not emit any unnecessary bounds checks:

  for i in some_arr {
    println!("{i}");
  }

I suspect most techniques you could think of to statically avoid bounds checks are possible in rust's type system.

▲ uecker an hour ago | parent [-]

These are not terribly interesting cases though, as it would also be impossible to get an oob access in other languages either.

▲ wasmperson 36 minutes ago | parent [-]

Yes, rust didn't invent the concept of an iterator, and is thus not the only language which offers a solution to statically avoid bounds checks. Feel free to give a more "interesting" case you believe rust wouldn't be able to handle.

	▲	uecker 11 minutes ago \| parent [-]
		Rust fails to prove basic indirection to be statically safe and instead does a run-time check. `fn main() { let v = vec![1, 2, 3]; v[5]; }`

▲ LoganDark 3 hours ago | parent | prev [-]

It's possible to do this (WUFFS does it) but it's so invasive that, well, you basically end up with WUFFS. You end up having to track every set of possible and impossible values at every location, etc. (during each program location too.) WUFFS certainly has its place and I've kind of been itching to try it out myself, but I think getting to the point where dynamic arrays can be statically bounds-checked would have highly disabled Rust.