12 ms·
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 hal
by 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 agoI'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]); }
- dwattttt 1y agoAt compile time, Rust guaranteed memory safety here by ensuring a runtime check was present, which your code triggered, resulting in a panic. A panic is not a violation of memory safety; if you wanted to violate memory safety you'd need to have caused that deref to succeed, and println to spit out the result. EDIT: let me guess, did the panic message include "index out of bounds: the len is 5 but the index is 10"?
- bgwalter 1y agohttps://news.ycombinator.com/item?id=45882148 https://news.ycombinator.com/item?id=45882148
- mustache_kimono 1y ago> but rustc-1.63.0 still compiles this program that panics at runtime. An index OOB error? Here, it's important to remember the Rust panic is still memory safe. Perhaps you should read the article, or read up on what undefined behavior is?[0] Here, the Rust behavior is very well defined. It will either abort or unwind.[1] If you prefer different behavior, there is the get method on slices.[2] [0]: https://en.wikipedia.org/wiki/Undefined_behavior https://en.wikipedia.org/wiki/Undefined_behavior [1]: https://doc.rust-lang.org/reference/panic.html https://doc.rust-lang.org/reference/panic.html [2]: https://doc.rust-lang.org/std/primitive.slice.html#method.get https://doc.rust-lang.org/std/primitive.slice.html#method.ge...
- bgwalter 1y agoThis subthread is about claims of STATIC checking of memory safety. A panic is not static checking. Perhaps you should read what you respond to.
- unrealhoang 1y agoA panic is memory-safe, so static checking of memory safety holds. Perhaps you should understand your own claims.