[wasmperson]

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]

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];
  }

[steveklabnik]

If this was an array, that is, a built-in type with a static length, this example does give a compile-time error: https://play.rust-lang.org/?version=stable&mode=debug&editio...

However, a vector's length is inherently a runtime concept, and is a user-defined library type, so the compiler does not attempt to directly reason about this at compile time. However, for this example, post-optimizations, it doesn't do a runtime check at all: it calls the panic directly, because the optimizer does in fact reason that this always panics and removes the dynamic check.

It is true that Rust inserts dynamic checks for things that it can't prove statically, but so do dependently typed languages. "Please read an integer from stdin and then load that element of an array" is not possible to statically check, it must rely on runtime checks, definitionally.

[uecker]

A: "Rust prefers to prevent all undefined behavior statically"

me: It does dynamic bounds checking.

Rustaceans: But... for XYZ ... it doesn't...

Sigh.

[steveklabnik]

It's because you're not using words in the way that people use them when talking about this stuff.

Rust (outside of the unsafe superset) has no undefined behavior. That is guaranteed, statically, at compile time: all execution paths have well-defined behaviors. That does not mean that there are no runtime consequences whatsoever. For example, the behavior of an invalid index is a panic, at runtime. Inserting a check for an invalid index at compile time is static enforcement of the behavior, even if the check itself happens at runtime.

If you had said "sometimes, Rust can't eliminate dynamic checks because it doesn't have a strong enough reasoning about some compile time properties" nobody would be arguing with you about this. Your example is one where a language with stronger reasoning would be able to detect it, for sure. Lean can do this, for example.

[uecker]

Rust does not do prevent all UB statically. Even if you guarantee at compile-time that all execution paths have well-defined semantics because compiler inserted run-time checks, this is not the same thing as "statically ensuring the absence of this run-time condition that would cause UB" which would be what people usually mean with "statically preventing UB". So I think it is not me who uses the works in an unusual way.

If, of course, you redefined words so that adding run-time checks counts as "statically preventing all UB", then this applies to Fil-C just as well! You can not have it both ways.

[josephg]

These are all true? I don’t see the problem?

Rust does prefer static checks. It uses static analysis to prevent many types of bugs - including use-after-free and data races. But you’re right; rust still falls back to runtime checks when static analysis is too hard. Like dynamic bounds checking and integer overflow (in debug mode). Cell, Refcell and friends also have a (small) runtime cost. Rust prefers static analysis but does not use it exclusively.

Let’s say rust is 80% static analysis, 20% dynamic checks. Fil-C seems to go the other way and have 80+% dynamic checks. It’s an interesting point.

Nobody disagrees with you that rust sometimes inserts dynamic bounds checks. But “prefer” in this context means “most of the time, when possible” not “all of the time”. I prefer vanilla ice cream over chocolate. But I still eat chocolate ice cream when vanilla isn’t available. Pointing out that one time I ate chocolate ice cream isn’t a gotcha moment.

[uecker]

If we can all agree that my statement was true, there is no problem.

[wasmperson]

Now it's your example that's too simple. I can't present a counter-example that wouldn't look totally different: if you avoid the indexing operator then trivially incorrect code like that becomes unrepresentable. It's like if I said destructors help you avoid memory leaks and you asked how you'd avoid a leak in a single-function program that does nothing but call `Box::leak()`.

Again: I'm not disputing the fact that the rust index operator does a dynamic bounds check.

[uecker]

If you agree with that Rust sometimes has to add dynamic bounds check, then you could have just agreed with my original comment.