Obtaining a computational history of a Turing Machine I am currently reading the proof presented in Sipser's "Theory of Computation" for the undecidability of the problem of checking whether the language accepted by a linear bounded automata is empty. In this proof, a contradiction is derived via a reduction from the problem of checking whether a Turing machine, $M$ accepts a given input, $w$. The proof seems to use the fact that from an input in the form $\langle M,w \rangle$, it is always possible to get a computational history, $C$, of $w$ when run on $M$. Then, $C$ is fed into some LBA, $B$, which checks if its input is an accepting configuration of $M$.

It seems to me that in order to obtain $C$ in the first place, we must simulate $M$ on $w$. However, if $M$ does not halt (and since $M$ is not an LBA, it is not guaranteed that there are a finite number of configurations), then we will never obtain $C$ (and $C$ would not be finite). It seems that the problem of obtaining a computational history of a Turing machine is equivalent to checking whether a Turing machine accepts its input. So what is the method used to always obtain $C$ from $M$ and $w$? Don't we need to prove the existence of such a method if we are going to use it to derive a contradiction?
It is correct that you cannot compute $C$ in case $M$ does not halt on $w$.

What can be done is to query $C$, that is for a given time $t$ to compute the $t$-th configuration of $M$ on input $w$. Also, you can compute finite prefixes of $C$ of given length. Possibly, these operations are already sufficient for the proof in the book that you read (which I did not read).

Also, from the outline you give it seems that it is not necessary to compute $C$ at all. If $M$ accepts $w$, there is a finite $C$ which will be recognized by $B$. The reduction has to compute $B$ from $M$ and $w$, not $C$ itself. $C$ is just the input that would witness non-emptyness of $L(B)$.