Given a sequence of reals $(a_n)_{n=0}^\infty$, we can define a subsequence of it to be computable if the set of its indexes is a computable set.
using this definition it's not too hard to see that there is a bounded sequence without a computable convergent subsequence: you can, for example, construct $A \subseteq \mathbb{N}$ that intersects every computable set infinitely many times and whose complement intersects every computable set infinitely many times, and define $$a_n = \begin{cases} \displaylines{ 1, n \in A \\ 0, n \notin A} \end{cases}$$ A computable subsequence must have infinitely many $1$'s and $0$'s, so it diverges.
So instead, we define a subsequence to be computable if the set of indixes of it is computable given the sequence $(a_n)_{n=0}^\infty$. More precisely, a set of naturals is computable given $(a_n)_{n=0}^\infty$ if there is a Turing machine that computes it that can use an oracle that, given $n,m \in \mathbb N$, returns the $m$'th digit of $a_n$. This basically means that we can do arbitrary precision calculations on $a_n$.
With this definition, the previous example has a computable convergent subsequence: the constant sequence $1$.
My question is: is there a bounded sequence with no computable convergent subsequence?
The only results I got are:
$\bullet$ Any sequence with a computable partial limit has a c.c.s, as a program can iterate over the indexes and include ones with images "close enough" to the computable limit, where "close enough" approaches $0$ as more indexes are added. Here the "close enough" calculation is done using the oracle.
$\bullet$ Any sequence with an isolated partial limit has a c.c.s, as there is a rational interval around the partial limit with no other partial limits, and a program can simply include all indixes with images inside this interval (perhaps discarding images "too close" to the ends of the interval because equality is uncomputable; this is not a serious problem).
So such a sequence would need to have an interesting set of partial limits, with no isolated points but not dense on any interval (since the set of partial limits is always closed and can't contain computable numbers).
There exists a computable sequence of reals $(x_n)_{n \in \mathbb{N}}$ in $[0,1]$ such that no accummulation point is computable from $\emptyset'$ (the Halting problem). Any convergent computable sequence has a limit point which is computable from $\emptyset'$, thus our sequence $(x_n)_{n \in \mathbb{N}}$ cannot have any convergent computable subsequences.
Further reading:
Brattka, Gherardi & Marcone: The Bolzano-Weierstrass Theorem is the Jump of Weak König's Lemma. Annals of Pure and Applied Logic 2012
https://doi.org/10.1016/j.apal.2011.10.006 or https://arxiv.org/abs/1101.0792