zlacker

> but Rust also has no built-in mechanism to statically determine “this code won’t ever panic”,

My intuition says that's the Halting Problem, so not actually possible to implement perfectly? https://en.wikipedia.org/wiki/Halting_problem

>>jrochk+(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).

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.

>>jrochk+(OP)
If you are fine with saying that stuff like this code may panic (and many people are fine with just that), then it's perfectly doable

    if false {
        panic!()
    }

Basically you'd prohibit any call to panic whether they may actually end up running or not.

>>jrochk+(OP)
That's different. You can't perfectly detect all infinite loops in a language that allows arbitrary loops. This also means you can't perfectly detect unreachable code.

But determining that a function (such as panic) is never called because there are no calls to it is pretty easy.

>>jrochk+(OP)
No, panic is not halting, you just need some static check to check that you never call some functions that can panic in your code. Essentially it is just checking if some code (panic) might be reachable, if it is not, it will never panic (but it can still do other crazy things).

Note that we can only check for maybe, because in general we don't know if some code in the middle will somehow execute forever and never reach the panic call after it.

>>jrochk+(OP)
See https://news.ycombinator.com/item?id=33057059.

>>pca006+72
Even if it is halting, you can sometimes statically detect if a Turing machine never halts. Just look through the state machine and see if any states will transition to a halt; if none of them do, the machine will loop forever. This is not a very large fraction of machines that loop forever, but if you're writing a machine and want to be absolutely sure it won't halt, just don't put in any states that halt.

>>jmilli+p1
> 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.

>>gpm+I6
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.

>>im3w1l+D1
Fair. From the responses, clearly i didn't know what I was talking about, fair enough!

But ok, uninformed me would have guessed checking for that would be pretty straightforward in statically typed Rust. Is that something people want? Why isn't there a built-in mechanism to do it?