Nonstandard analysis is a useful tool which can be used to prove a number of results in analysis.  



Question
--------

 

> Can it also be used to prove results in computable or constructive analysis?
>
> If so, what are some examples?  (They don't need to be ground-breaking.)




Motivation
----------

There seems to be this analogy involving small worlds and big worlds (*model* is probably a more accurate term).

computable math

 - small: computable real numbers 
 - big: real numbers

nonstandard analysis: 
 
 - small: standard real numbers
 - big: nonstandard real numbers

This analogy is quite common in logic (ground model vs forcing extension for another example).

Can statements about the computably of finite objects be moved to the "computability" of nonstandard finite objects, and then transferred to the computability of standard infinite objects?

I am aware of Sam Sanders' program to connect Bishop-style constructive analysis with nonstandard analysis, but I am not aware (possibly mistakenly) that it has been used to prove statements in computable/constructive mathematics.

Possible examples
------
> 1. Can one use nonstandard analysis to show that the supremum of a computable function $f$ on $[0,1]$ is computable uniformly from $f$?  (The corresponding finitary statement about finite functions of rationals is clearly true.)
>
> 2. What about the computability of the Riemann integral?