It is well know that each Borel measure m on metric space is regular, i.e. for Borel set A and any d>0 there are open set G and close set F, such that F\subset A\subset G and m(G\F)
Regularity is important in the description of multiscale measures and functions. This is central theme in
M.L Lapidus, J.A. Rock, Toward zeta functions and complex dimensions of multifractals, arXiv 0810, 2008, no. 0789v1, 1-16, downloadable from RG.
The regularity of a Borel measure is defined on page 3 (see Def. 2.1). Partition zeta functions are introduced in Section 4, starting on page 8, defined for any Borel measure. See Theorem 5.2, starting on page 12, the regularity of a Borel measure is considered.
Reverse mathematics is considered in proving the measure-theoretic regularity in the Borel hierarchy in
S.G. Simpson, Mass problems and measure-theoretic regularity, Penn. State University, 2014:
Regularity is important in the description of multiscale measures and functions. This is central theme in
M.L Lapidus, J.A. Rock, Toward zeta functions and complex dimensions of multifractals, arXiv 0810, 2008, no. 0789v1, 1-16, downloadable from RG.
The regularity of a Borel measure is defined on page 3 (see Def. 2.1). Partition zeta functions are introduced in Section 4, starting on page 8, defined for any Borel measure. See Theorem 5.2, starting on page 12, the regularity of a Borel measure is considered.
Reverse mathematics is considered in proving the measure-theoretic regularity in the Borel hierarchy in
S.G. Simpson, Mass problems and measure-theoretic regularity, Penn. State University, 2014:
This is a very amateur answer, but I'd recommend Palmgren's works on constructive measure theory. I think you may require "fixing" of the regularity theorem, i.e. additional assumptions, since even metric spaces themselves are treated quite different, as in classical math (see Bishop&Bridges for instance). In particular, one cannot quantify over arbitrary open sets. I think even the measure itself is not computable in general.
I think that I have a proof. According to my study, the finite Borel measure on a metric space is a metric measure space (i.e. regular) if the metric space is locally compact and separable. The condition on the metric space is pretty strong. In this case, I have a constructive proof.
I managed to find what you need. See "Approximating integrable sets by compact sets constructively" (2005) by Spitters, Section 4 and in particular Theorem 4.3. It will tell you what additional assumptions are needed to "fix" the theorem.