Elementary proof of compact space = exhaustible space? (This is a repost of a question I asked last year on cs.stackexchange.)

The work of Martín Escardó has demonstrated close parallels between classical topology on one hand and computability on the other hand.  (See for example "Infinite sets that admit fast exhaustive search" 22nd Annual IEEE Symposium on Logic in Computer Science (2007)  443–452)
Escardó identifies continuous functions with computable functions, and open sets with recursively enumerable sets.
Another identification is between the exhaustible sets on one hand and compact sets on the other.  A set $S$ is exhausible if, given a total predicate $P:S\to\mathbf{Bool}$, one can always decide whether $P$ holds for every element of $S$.  According to Escardó, there is a close relationship between exhaustible and compact sets.  For example:


*

*Finite sets are both compact and also obviously exhaustible.

*The natural numbers are not compact and are not exhaustible. (If they were, we could solve the halting problem.)

*But the one-point compactification of the naturals is exhaustible.

*The Cantor set of all sequences of booleans, that is all functions $f:\Bbb N\to\mathbf{Bool}$ is both compact and exhaustible.


I have found the discussion of compactness in Escardó's papers very hard to follow, with many forward references.  The nearest thing to a proof that I can identify is in section 8 of his notes on "synthetic topology of data types". The proof in chapter 8 is very advanced.  In these notes compactness is initially defined to be exhaustibility, which doesn't make it easier to follow what is going on.
My question is:

I keep hoping for an elementary proof, one which relates the conventional definition of compactness, in terms of open covers, to exhaustibility. I have not been able to find one myself and I have not been able to extract one from Escardó's papers.  Is there such a proof?

 A: Compactness and exhaustibility is not the same thing, not even "morally". As an example, we can consider the reals. As $\mathbb{R}$ is connected, the only decidable predicates $P : \mathbb{R} \to \mathrm{Bool}$ are the constant ones. We can thus decide whether $P$ applies to all of $\mathbb{R}$ just by testing whether $P$ applies to $0$. So $\mathbb{R}$ is exhaustible, but for a boring reason.
So, how the two notions connected? First of all, an important caveat is that to make everything nice, we consider only hereditarily Lindelöf spaces. As a consequence, we don't need to distinguish compactness and countably compactness. Furthermore, we either work in constructive theory for the topological notions, or we relativize all of the computability notions w.r.t. some arbitrary oracle.
Now we can line up exhaustibility with compactness for zero-dimensional spaces. In a zero-dimensional space, any open cover has a refinement into disjoint clopen sets. Let us assume that $\mathbf{X}$ is zero-dimensional and not countably compact. Thus, we have $\mathbf{X} = \bigcup_{n \in \mathbb{N}} B_n$ for disjoint non-empty clopen $B_n$. Given a Turing machine $M$, define a predicate $P_M : \mathbf{X} \to \mathrm{Bool}$ as follows: From $x \in \mathbf{X}$ we can obtain the $n \in \mathbb{N}$ such that $x \in B_n$. Then return "yes" if $M$ does not halt in fewer than $n$ time steps, "no" otherwise. Now $P_M$ covers $\mathbf{X}$ iff $M$ never halts - thus, $\mathbf{X}$ is not exhaustible.
Conversely, if $\mathbf{X}$ is zero-dimensional, countably-based and countably compact, we shall see that $\mathbf{X}$ is exhaustible. If $\mathbf{X}$ is countably-based, it is also separable. Since $P^{-1}(\top)$ and $P^{-1}(\bot)$ are disjoint open sets in $\mathbf{X}$ for any predicate $P : \mathbf{X} \to \mathrm{Bool}$, we know that $P$ applies to all of $\mathbf{X}$ iff it applies to every point in the dense sequence $(a_n)_{n \in \mathbb{N}}$ we have from separability. We begin testing $P(a_n)$ for all $n \in \mathbb{N}$. If we ever get $\bot$, we answer $\bot$. Whenever we learn that $P(a_n) = \top$, we actually learn that $P$ returns $\top$ for all $x \in B_k$ for a basic open $B_k$ by continuity. By countably compactness of $\mathbf{X}$, if the $B_k$ we find like this cover $\mathbf{X}$, already finitely many of them do. Thus, at some finite step of this process we will have learned enough information to confirm that $P$ applies to all of $\mathbf{X}$.
If we want to define compactness in manner similar to exhaustibility, without the requirement to restrict to zero-dimensional spaces, we need to consider semi-decidable properties, not decidable properties. We thus use Sierpinski space $\mathbb{S}$ in place of $\mathrm{Bool}$. Compactness then becomes "We can recognize that a recognizable predicate applies to every element of the space" or equivalently, $\{X\}$ is an open singleton in the space $\mathcal{O}(\mathbf{X})$ of open subsets of $\mathbf{X}$.
My attempt to explain this approach to compactness (with some proofs) can be found in this paper:
Arno Pauly: "On the topological aspects of the theory of represented spaces", Computability, 2016: doi: 10.3233/COM-150049
My article does not cover exhaustibility, though.
