  Topology may be interpreted as the study of verifiability, where opens
correspond to semi-decidable properties. In this paper we make a distinction
between verifiable properties themselves and processes which carry out the
verification procedure. The former are simply opens, while we call the latter
machines. Given a frame presentation $\mathcal{O} X = \langle G \mid R\rangle$
we construct a space of machines $\Sigma^{\Sigma^G}$ whose points are given by
formal combinations of basic machines corresponding to generators in $G$. This
comes equipped with an `evaluation' map making it a weak exponential for
$\Sigma^X$.
  When it exists, the true exponential $\Sigma^X$ occurs as a retract of
machine space. We argue this helps explain why some spaces are exponentiable
and others not. We then use machine space to study compactness by giving a
purely topological version of Escard\'o's algorithm for universal
quantification over compact spaces in finite time. Finally, we relate our study
of machine space to domain theory and domain embeddings.
