zlacker

You can prove that a machine can't ever write "1" to the tape if you just look at the state machine and see that none of the rules write a 1 to the tape. Since no rules ever write 1, no possible execution could.

Working out whether it will write 1 to the tape in general is undecidable, but in certain cases (you've just banned states that write 1) it's trivial.

If all of the state transitions are valid (a transition to a non-existing state is a halt) then the machine can't get into a state that will transition into a halt, so it can't halt. That's a small fraction of all the machines that won't halt, but it's easy to tell when you have one of this kind by looking at the state machine.

>>roywig+(OP)
"Print 1" is trivial according to this: https://en.wikipedia.org/wiki/Rice%27s_theorem.

But day to day programs are not trivial... as for your example, just switch it with this code: `print(gcd(user_input--,137))`... now it's quite more hard to "just ban some final states"

>>yonixw+jd
Indeed, but panic is easier because in some ways checking if a program can panic is akin to checking if the program links the panic function.

And that's pretty easy to statically analyze.

>>yonixw+jd
That's not what "trivial property" means w.r.t. Rice's Thm.

The point is that you can produce a perfectly working analysis method that is either sound or complete but not both. "Nowhere in the entire program does the call 'panic()' appear is a perfectly workable analysis - it just has false positives.

>>yonixw+jd
Turing machines have a set of states and a transition function that governs how it moves between states. The transition function is a bunch of mappings like this:

    (input state, input symbol) --> (output state, output symbol, move left/right)

This is all static, so you can look at the transition table to see all the possible output symbols. If no transition has output symbol 1, then it never outputs 1. It doesn't matter how big the Turing machine is or what input it gets, it won't do it. This is basically trivial, but it's still a type of very simple static analysis that you can do. Similarly, if you don't have any states that halt, the machine will never halt.

This is like just not linking panic() into the program: it isn't going to be able to call it, no matter what else is in there.

>>roywig+(OP)
> Rust is arguably less safe in that aspect than C, due to the general Rust practice of panicking upon unexpected conditions

For context, this is OP's sentence that I responded to in particular. Ensuring safety [1] is way less trivial than looking for a call to "panic" in the state machine. You can remove the calls to "panic" and this alone does not make your program safer than the equivalent C code. It just makes it more kernel friendly.

[1] not only memory safety