Correct me if I slept in my computer science studium: If an automaton is Turing-equivalent, the Halting problem shows that there are programs we can not verify (since we can't even predict their output in the first place).
Now, this is a theoretical result; in practice, software writers all over the world try to verify their programs and usually succeed. Can you give me an actual example of an automaton (Petri net, Turing machine, whatever), either...
a) one which no human understands at all, or even better (since we could cheat in "a" by simply adding complexity until our brain gives up)
b) one which is fully understood by human but nobody can prove the actual behavior.
(It's debatable whether checkmating with King, Rook, and Bishop against King, Knight, and Knight would already constitute a valid example, since I think it falls under the complexity cheat. And maybe "b" is a contradiction in terms.)

Correct me if I slept in my computer science studium: If an automaton is Turing-equivalent, the Halting problem shows that there are programs we can not verify (since we can't even predict their output in the first place).
Now, this is a theoretical result; in practice, software writers all over the world try to verify their programs and usually succeed. Can you give me an actual example of an automaton (Petri net, Turing machine, whatever), either...
a) one which no human understands at all, or even better (since we could cheat in "a" by simply adding complexity until our brain gives up)
b) one which is fully understood by human but nobody can prove the actual behaviour.
(It's debatable whether checkmating with King, Rook, and Bishop against King, Knight, and Knight would already constitute a valid example, since I think it falls under the complexity cheat. And maybe "b" is a contradiction in terms.)

Correct me if I slept in my computer science studium: If an automaton is Turing-equivalent, the Halting problem shows that there are programs we can not verify (since we can't even predict their output in the first place).
Now this is a theoretical result, in praxis software writers all over the world try to verify their programs and usually succeed. Can you give me an actual example of an automaton (Petri net, Turing machine, whatever), either...
a) one which no human understands at all, or even better (since we could cheat in "a" by simply adding complexity until our brain gives up)
b) one which is fully understood by human but nobody can prove the actual behaviour.
(It's debatable whether checkmating with KRB against KNN would already constitute a valid example, since I think it falls under the complexity cheat. And maybe "b" is a contradiction in terms.)

Correct me if I slept in my computer science studium: If an automaton is Turing-equivalent, the Halting problem shows that there are programs we can not verify (since we can't even predict their output in the first place).
Now, this is a theoretical result; in practice, software writers all over the world try to verify their programs and usually succeed. Can you give me an actual example of an automaton (Petri net, Turing machine, whatever), either...
a) one which no human understands at all, or even better (since we could cheat in "a" by simply adding complexity until our brain gives up)
b) one which is fully understood by human but nobody can prove the actual behavior.
(It's debatable whether checkmating with King, Rook, and Bishop against King, Knight, and Knight would already constitute a valid example, since I think it falls under the complexity cheat. And maybe "b" is a contradiction in terms.)