zlacker

[parent] [thread] 2 comments
1. jmilli+(OP)[view] [source] 2022-10-02 16:01:40
If you were to define a subset of Rust's standard library (core + alloc + std) that does not contain the `panic!` macro, and excluded all functionality that needed to panic, then safe Rust could be proven to never panic (because it can't).

That's different than solving the halting problem. You're not trying to prove it halts, you're just trying to prove it doesn't halt in a specific way, which is trivial to prove if you first make it impossible.

replies(1): >>gpm+j5
2. gpm+j5[view] [source] 2022-10-02 16:29:01
>>jmilli+(OP)
> If you were to define a subset of Rust's standard library (core + alloc + std) that does not contain the `panic!` macro, and excluded all functionality that needed to panic, then safe Rust could be proven to never panic (because it can't).

Not quite, because stack overflows can cause panics independent of any actual invocation of the panic macro.

You need to either change how stack overflows are handled as well, or you need to do some static analysis of the stack size as well.

Both are possible (while keeping rust turing complete), so it's still not like the halting problem.

replies(1): >>jmilli+68
◧◩
3. jmilli+68[view] [source] [discussion] 2022-10-02 16:41:57
>>gpm+j5
In a Rust defined without `panic!`, a stack overflow would not be able to panic. What would probably happen is the process would just die, like C.
[go to top]