Hey great presentation guys.
I just wanted to add that contrary to what was said in the video, Finite Automata do not necessarily have a guaranteed acceptance state for any arbitrary input sequence. Repeating states with cycles of different sizes may be perfectly valid (i.e. one may want a FA for its side effects only). The “Finite” term there refers to the number of states in the machine. What guarantees you termination is the general definition for Deterministic FAs which requires a non-empty set of acceptance states.
And without touching the proof by contradiction the most simple intuition behind the halting problem is not that you may trick the analyzer into returning the wrong result but that any analyzer would have to be able to evaluate all possible states and transitions of a program to determine if it would ever come to an end which is basically the same as to say the analyzer would have to run the original program itself. Since the hypothesis is that the original program may never end we get stuck back where we started…