This is not strictly an answer to the history question, but I would like to take this opportunity to record my dissent from the common assertion that compactness is about finiteness.

I claim instead that compactness is about covering.

Consider the relation $K\subset U$ as a function (predicate) of the argument $U$ ranging over open subspaces. This function is continuous in $U$ (with respect to the Scott topology) iff $K$ is compact.

If you haven't heard of the Scott topology before, you can take this equivalence as its definition (assuming that you know the usual one for compactness!).

When we also consider membership $x\in U$ as a predicate $\phi(x)$, the containment $K\subset U$ becomes $\forall x:K.\phi(x)$.

So a compact subspace is one over which we may perform universal quantification.

The dual treatment of the existential quantifier is described, using the novel notion of overtness in this answer by @Andrej Bauer, and the additional one by me tries to relate the idea to familiar ones such as the Newton-Raphson algorithm.

In print, compactness and overtness in $\mathbb R$ are explored in the paper by Andrej and me and the further one of mine.

This is not strictly an answer to the history question, but I would like to take this opportunity to record my dissent from the common assertion that compactness is about finiteness.

I claim instead that compactness is about covering.

Consider the relation $K\subset U$ as a function (predicate) of the argument $U$ ranging over open subspaces. This function is continuous in $U$ (with respect to the Scott topology) iff $K$ is compact.

If you haven't heard of the Scott topology before, you can take this equivalence as its definition (assuming that you know the usual one for compactness!).

When we also consider membership $x\in U$ as a predicate $\phi(x)$, the containment $K\subset U$ becomes $\forall x:K.\phi(x)$.

So a compact subspace is one over which we may perform universal quantification.

The dual treatment of the existential quantifier is described, using the novel notion of overtness in this answer by @Andrej Bauer, and the additional one by me tries to relate the idea to familiar ones such as the Newton-Raphson algorithm.

In print, compactness and overtness in $\mathbb R$ are explored in the paper by Andrej and me and the further one of mine.