6 ms·

TFA is too long, like all articles since the arrival of you know what. So the definitions are scattered. Here it claims: Rust's big step function was to offer

TFA is too long, like all articles since the arrival of you know what. So the definitions are scattered. Here it claims: Rust's big step function was to offer memory safety at compile time through the use of static analysis borrowed and grown out of prior efforts such as Cyclone, a research programming language formulated as a safe subset of C. In other words, Rust has solved the halting problem since the static checking of array bounds is undecidable in the general case!

Jtsummers 1y ago
> In other words, Rust has solved the halting problem No one is making that claim.
- bgwalter 1y ago
  "offer memory safety at compile time through the use of static analysis" For arrays, this problem is not computable at compile time, hence the sarcastic remark that, IF THE ABOVE DEFINITION IS TAKEN AT FACE VALUE, Rust must have solved the halting problem. Downvoters are so dumb here.
  - deleted 1y ago
    [deleted]
  - Jtsummers 1y ago
    > IF THE ABOVE DEFINITION IS TAKEN AT FACE VALUE Why are you shouting? That's what twits do. You don't want to be a twit, do you? Read the site guidelines, emphasis is done with italicized text marked up with an * at the beginning and another * at the end. But to respond to the topic at hand: Are you familiar with the distinction between sound (what Rust aims for) and complete analyses?
    - bgwalter 1y ago
      Are you familiar with the fact that Rust does array bounds checking at runtime, contrary to the cited claim? And that this was kind of the topic of this subthread? https://stackoverflow.com/questions/28389371/why-does-rust-check-array-bounds-at-runtime-when-most-other-checks-occur-at-c https://stackoverflow.com/questions/28389371/why-does-rust-c...
      - deleted 1y ago
        [deleted]
      - deleted 1y ago
        [deleted]
      - vlovich123 1y ago
        Are you aware you’ve built a straw man and replied to it? Literally you quoted: > Rust's big step function was to offer memory safety at compile time through the use of static analysis borrowed and grown out of prior efforts such as Cyclone, a research programming language formulated as a safe subset of C. It is absolutely true that memory safety is offered at compile time in Rust which is a novel thing. You then pivoted this to start talking about bounds safety of arrays which is a strawman interpretation of what was written.
        bgwalter 1y ago
        Bounds checking is part of "memory safety" and Rust people don't get the monopoly on that term. The definition of "memory safety" is literally the topic of this subthread.
        bgwalter 1y ago
        I did not pivot. TFA itself defines: "Memory safety—the property that makes software devoid of weaknesses such as buffer overflows, double-frees, and similar issues—has been a popular topic in software communities over the past decade" And the buffer overflows are not detected statically except for the cases when the compiler can prove them. And Rust proponents keep ignoring the topic of this subthread, which is memory safety by static analysis.
        vlovich123 1y ago
        As others have pointed out to you. Memory safety is enforced at compile time through static analysis. This does not mean the absence of runtime checks - that is a property you are injecting into the definition and arguing about. RefCell enforces memory safety too by doing the lifetime enforcement at runtime by using UnsafeCell to provide certain semantics. But the compiler ensures that the RefCell itself still has correct lifetimes and is used correctly, resulting in a compile time guarantee that the code that’s run is memory safe.
tialaramex 1y ago
Nope. You don't need to "solve the halting problem" and I guess I'll explain why here. Firstly lets attack the direct claim. The reason you'd reduce to the halting problem is via Rice's theorem. But, Rice only matters if we want to allow exactly all the programs with the desired semantics. In practice what you do is either allow some incorrect programs too (like C++ does, that's what IFNDR is about, now some programs have no defined behaviour at all, but oh well, at least they compiled) or you reject some correct programs too (as Rust does). Now what we're doing is merely difficult rather than provably impossible, and people do difficult things all the time. This is an important choice (and indeed there's a third option but it's silly, you could do both, rejecting some correct programs while allowing some incorrect ones, the worst of both worlds) but in neither case do we need to solve an impossible problem. Now, a brief aside on what Rust is actually doing here, because it'll be useful in a moment. Rust's compiler does not need to perform a static bounds check on array index, what Rust's compiler needs to statically check is only that somebody wrote the runtime check. This satisfies the requirement. But now back to laughing at you. While in Rust it's common to have fallible bounds checks at runtime (only their presence being tested at compile time) in WUFFS it's common for all the checks to be at compile time and so to have your code rejected if the tools can't see why your indexing is always in bounds. When WUFFS sees you've written arr[k] it considers this as a claim that you've proved 0 <= k < arr.len() if it can't see how you've proved that then your code is wrong, you get an error. The result is that you're going to write a bunch of math when you write software, but the good news is that instead of going unread because nobody reviewing the code bothered reading the maths the machine read your math and it runs a proof checker, so if you were wrong it won't compile. Edited: Fix off-by-one error
- bgwalter 1y ago
  I'm glad that I provide amusement, but rustc-1.63.0 still compiles this program that panics at runtime. My experience with Rust is 5 min, so the style may provide further amusement: fn f(n : usize) -> usize { if n == 0 { 10 } else if n % 32327 == 0 { 1 } else { f(n-1) } } fn main() { let a = [1,2,3,4,5]; let n = f(12312); println!("{:?}", a[n]); }
  - 1y ago
lmm 1y ago
> In other words, Rust has solved the halting problem since the static checking of array bounds is undecidable in the general case! Pfft, the simply typed lambda calculus solved the halting problem back in 1940.

Jtsummers 1y ago

> In other words, Rust has solved the halting problem No one is making that claim.

bgwalter 1y ago
"offer memory safety at compile time through the use of static analysis" For arrays, this problem is not computable at compile time, hence the sarcastic remark that, IF THE ABOVE DEFINITION IS TAKEN AT FACE VALUE, Rust must have solved the halting problem. Downvoters are so dumb here.
- deleted 1y ago
  [deleted]
- Jtsummers 1y ago
  > IF THE ABOVE DEFINITION IS TAKEN AT FACE VALUE Why are you shouting? That's what twits do. You don't want to be a twit, do you? Read the site guidelines, emphasis is done with italicized text marked up with an * at the beginning and another * at the end. But to respond to the topic at hand: Are you familiar with the distinction between sound (what Rust aims for) and complete analyses?
  - bgwalter 1y ago
    Are you familiar with the fact that Rust does array bounds checking at runtime, contrary to the cited claim? And that this was kind of the topic of this subthread? https://stackoverflow.com/questions/28389371/why-does-rust-check-array-bounds-at-runtime-when-most-other-checks-occur-at-c https://stackoverflow.com/questions/28389371/why-does-rust-c...
    - deleted 1y ago
      [deleted]
    - deleted 1y ago
      [deleted]
    - vlovich123 1y ago
      Are you aware you’ve built a straw man and replied to it? Literally you quoted: > Rust's big step function was to offer memory safety at compile time through the use of static analysis borrowed and grown out of prior efforts such as Cyclone, a research programming language formulated as a safe subset of C. It is absolutely true that memory safety is offered at compile time in Rust which is a novel thing. You then pivoted this to start talking about bounds safety of arrays which is a strawman interpretation of what was written.
      - bgwalter 1y ago
        Bounds checking is part of "memory safety" and Rust people don't get the monopoly on that term. The definition of "memory safety" is literally the topic of this subthread.
      - bgwalter 1y ago
        I did not pivot. TFA itself defines: "Memory safety—the property that makes software devoid of weaknesses such as buffer overflows, double-frees, and similar issues—has been a popular topic in software communities over the past decade" And the buffer overflows are not detected statically except for the cases when the compiler can prove them. And Rust proponents keep ignoring the topic of this subthread, which is memory safety by static analysis.
        vlovich123 1y ago
        As others have pointed out to you. Memory safety is enforced at compile time through static analysis. This does not mean the absence of runtime checks - that is a property you are injecting into the definition and arguing about. RefCell enforces memory safety too by doing the lifetime enforcement at runtime by using UnsafeCell to provide certain semantics. But the compiler ensures that the RefCell itself still has correct lifetimes and is used correctly, resulting in a compile time guarantee that the code that’s run is memory safe.

tialaramex 1y ago

Nope. You don't need to "solve the halting problem" and I guess I'll explain why here. Firstly lets attack the direct claim. The reason you'd reduce to the halting problem is via Rice's theorem. But, Rice only matters if we want to allow exactly all the programs with the desired semantics. In practice what you do is either allow some incorrect programs too (like C++ does, that's what IFNDR is about, now some programs have no defined behaviour at all, but oh well, at least they compiled) or you reject some correct programs too (as Rust does). Now what we're doing is merely difficult rather than provably impossible, and people do difficult things all the time. This is an important choice (and indeed there's a third option but it's silly, you could do both, rejecting some correct programs while allowing some incorrect ones, the worst of both worlds) but in neither case do we need to solve an impossible problem. Now, a brief aside on what Rust is actually doing here, because it'll be useful in a moment. Rust's compiler does not need to perform a static bounds check on array index, what Rust's compiler needs to statically check is only that somebody wrote the runtime check. This satisfies the requirement. But now back to laughing at you. While in Rust it's common to have fallible bounds checks at runtime (only their presence being tested at compile time) in WUFFS it's common for all the checks to be at compile time and so to have your code rejected if the tools can't see why your indexing is always in bounds. When WUFFS sees you've written arr[k] it considers this as a claim that you've proved 0 <= k < arr.len() if it can't see how you've proved that then your code is wrong, you get an error. The result is that you're going to write a bunch of math when you write software, but the good news is that instead of going unread because nobody reviewing the code bothered reading the maths the machine read your math and it runs a proof checker, so if you were wrong it won't compile. Edited: Fix off-by-one error

bgwalter 1y ago
I'm glad that I provide amusement, but rustc-1.63.0 still compiles this program that panics at runtime. My experience with Rust is 5 min, so the style may provide further amusement: fn f(n : usize) -> usize { if n == 0 { 10 } else if n % 32327 == 0 { 1 } else { f(n-1) } } fn main() { let a = [1,2,3,4,5]; let n = f(12312); println!("{:?}", a[n]); }
- 1y ago

lmm 1y ago

> In other words, Rust has solved the halting problem since the static checking of array bounds is undecidable in the general case! Pfft, the simply typed lambda calculus solved the halting problem back in 1940.