Are files download times actually unknowable due to the halting problem? When downloading a file from the internet to our computer we are usually prompted with an estimate of how long it will take for the file to be downloaded.
From the Halting Problem, we know that $\mathrm{HALT}_{\mathrm{TM}}$ is undecidable, where:
$\mathrm{HALT}_{\mathrm{TM}} =\{⟨M,w⟩\mid M \text{ is a TM and }M\text{ halts on input }w \} $
Assuming that we can neglect the lack of infinite memory, we can model our computer writing on the disk as a Turing Machine $M$ and take the string encoding of the downloaded file as the input $w$. (More precisely, $w$ should be the string obtained composing the packets sent by the network)
From the Halting Problem it follows that it's not only impossible to know when the download will end, it's even impossible to know whether the download will ever end.
So, are files download times actually unknowable due to the halting problem? If not, where the above reasoning fails?
Not at all.
The halting problem says it is impossible to decide whether an arbitrary turing machine with arbitrary input will halt. But there are many, many specific turing machines where we can prove that they halt for every input, or where we can look at the input and decide if the turing machine will halt or not.
And since the people writing the download code surely wrote it in such a way that it is guaranteed to finish for every import, there will be a proof that it is guaranteed to finish.