A direct proof (using net convergence) that sequential compact metric space is compact

There is a reasonably direct proof of this fact. The trick is to take a subnet that is a sequence.

Consider a nonempty net $(x_d)_{d \in D}$. If there is a maximal $d$, then the singleton net $x_d$ converges to $d$. Otherwise, for every $d$, there is some greater $d’$. Using dependent choice, choose $d_1 < d_2 < \ldots$. Then $(x_{d_n})_{n \in \mathbb{N}}$ has a convergent subsequence which is also a convergent subnet of the original net.

If you wish for a constructive proof that every sequentially compact space is compact, I’m afraid you’re going to be disappointed (though I haven’t ruled out the possibility that there’s a constructive proof that sequentially compact implies net compact).

We can show constructively that every compact space $X$ either has a point or is empty. For consider the open cover $\{X \mid \exists y (y \in X)\}$. This open cover has a finitely enumerator sub cover $U_1, \ldots, U_n$. If $n = 0$, then $X$ Is empty, while if $n > 0$, then $X$ has a point.

Now for any proposition $p$, consider the associated topological space $\{0 \mid p\}$. This space is sequentially compact (in fact, net compact) and has a point if and only if $p$.

If we could show this space is also compact constructively, then we would have proved the space is either empty or no empty, and thus $p \lor \neg p$. But this cannot be done constructively. So no constructive proof can exist.