David Roberts has rubbed the magic lamp and the genie appears!

Even though the notion of overtness does depend on the strength of the ambient logic, 
I believe the problem here is with the notion of metric space, rather than the choice of a model of mathematics.

The natural answer is that any metric space has enough points and is therefore necessarily overt.

I am inclined to think that any *whole* space in topology is in practice overt and the interesting question is what overt *sub*spaces look like.

We have a *monster* (in the sense of Lakatos) that you could use as you please on either side of this argument:
The set $A\subset{\mathbb N}$ of programs that don't terminate, with the discrete metric, is not overt.

We can do better than this. [Steve Vickers](https://www.cs.bham.ac.uk/~sjv/papersfull.php) has an alternative to the Cauchy completion in locale theory and formal topology. Like any metric topology, it has a basis of *balls* $B(x,r)$, where we may take the radii $r$ to be dyadic rationals and the centres $x$ to be (for example) points with dyadic rational coordinates.

(Since I mention Steve, in general he is interested in the *hyper*spaces of *all* overt or compact subspaces, which are called the lower and upper *powerdomains*. My interest, in constrast, is with *individual* overt subspaces.)

To the general mathematician, the idea of an *operator* $\lozenge$ that takes unions of open subspaces to the existential quantifier is not very familiar. However, it has a very natural equivalent form when we're working in a metric space constructed in the above way.

Define $d(x)< r \equiv \lozenge B(x,r)$. It is easy to show that this satisfies

$$ d(x)<  r'<  r \Longrightarrow d(x)<  r $$
$$ d(x)<  r \Longrightarrow \exists r'.d(x)<  r'<  r $$
$$ d(x,y)<  r \;\land\; d(y)<  s \Longrightarrow d(x)<  r+s $$
$$ d(x)<  r \;\land\; \epsilon\gt 0 \Longrightarrow
     \exists y.d(x,y)<  r \;\land\; d(y)< \epsilon $$
for any $\epsilon>0$

What this means is that $d:X\to\overline{\mathbb R}$ is an *upper semicontinuous* function,
or alternatively one that is valued in the *upper real numbers*.

This is the essence of the equivalence between overt and *located* subspaces (the latter are used in Bishop-style constructive analysis), which was stated by [Bas Spitters](https://arxiv.org/pdf/math/0703561.pdf). Unfortunately he only considered the case of *closed* overt/located subspaces; these are characterised by $d$ being valued in the ordinary (Euclidean, Dedekind, ...) real numbers.

The more general case is covered in my draft paper [*Overt Subspaces of ${\mathbb R}^n$*](\http://www.paultaylor.eu/ASD?overtrn).

The third condition above is the triangle law.   Under suitable conditions, the **Newton--Raphson algorithm** yields a function $\Delta(x)\cong |f(x)/\dot f(x)|$ that satisfies all the other conditions and a $d$ obeying all of them can easily be derived from it.

My intuition is that **an overt subspace is the solution-space of an algorithm**.  To justify this we need more examples from numerical analysis like Newton--Raphson, but that is very much not my subject.

On the other hand, Newton--Raphson actually yields more information than the $d$ function.

There are two possible responses to this:
* Maybe we should replace overtness with something more *quantitative*; or
* Maybe an algorithm could be *derived* from the *formula* for $\lozenge$ or $d$ together with the *proof* that it has the appropriate properties.

The second is not completely unreasonable:
An overt subspace is a generalisation of a point defined by a Dedekind cut or a completely prime filter.  Andrej Bauer pioneered some ideas for [*Efficient computation with Dedekind reals*](https://mapcommunity.github.io/ictp/presentation_files/Bauer_P.pdf) and had a prototype calculator called Marshall.

Given how widely used the notions of overt, located or recursively enumerable subspaces now are in the different constructive cults, really we ought to have a better story than "overtness is dual to compactness but classically invisible".  There ought to be a way of explaining the idea to "ordinary" (classical) mathematicians, in particular numerical analysts.

I have been trying to do this for more than a decade, but I think I'm the wrong person to do it, and probably we can't do it from the constructive side: somehow we have to kidnap a numerical analyst and inculcate them with this idea.

I still have this *draft* paper (above).  Probably I should just stop fussing and publish it.  Comments towards that are welcome.