Correct me if I slept in my computer science studium: If an automaton is Turingequivalent, 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.)

$\begingroup$ Note that there are famous mathematical problems that can be written as halting problem. Like Fermat's last theorem, four color theorem, golbach conjecture and probably much more. $\endgroup$– Lucas K.Apr 26 '17 at 19:10
(a) I think that "no human understands" what the current busiest $6$state Busy Beaver $2$symbol Turing Machine is doing while it prints out $3.5 \times 10^{18267}$ $1$'s before halting.
(b) This does not quite address your 2nd question as you phrased it, but there are several $5$state quiteBusy Beavers that are believed to loop, but no one can prove they loop, or prove they halt. A list of these irregular Turing Machines is maintained here.
Incidentally, just to illustrate the complexity of BusyBeaver questions, a $4888$state Turing Machine has been constructed which halts if and only if there is a counterexample to Goldbach's conjecture.
Yedidia, Adam, and Scott Aaronson. "A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory." arXiv:1605.04343 (2016). (arXiv Abstract.)

$\begingroup$ Shorter Turing machines with similar properties along the same lines are now known, including a 43state machine which halts if and only if there is a counterexample to Goldbach's conjecture, see scottaaronson.com/blog/?p=2741 $\endgroup$ Apr 26 '17 at 22:02


$\begingroup$ (Now 27?) Wow. The Blog answers much more than I even asked. I wonder if verification tools for concrete Turing automata exist (analogous to the situation with higher Petri nets). $\endgroup$ Apr 27 '17 at 12:07
An oftencited example of a very basic program, for which termination is open, is one that generates the Collatz sequence. In pseudocode:
collatz(int n)
while (n > 1)
if (n mod 2 == 0)
n = n / 2;
else
n = 3n + 1;

2$\begingroup$ You want n>1, otherwise you can prove non termination with n!=0. Gerhard "Sees A Really Tight Loop" Paseman, 2017.04.26. $\endgroup$ Apr 26 '17 at 19:56

1