Nonstandard Analysis (NSA) can be used to prove results in computable/constructive analysis; The central notion is $\Omega$-invariance, defined as follows.

[As usual, the set $N$ consists of the standard/finite/natural numbers; The set ${^{\star}}N$ is an end-extension of $N$ and $\Omega={^{\star}}N\setminus N$ consists of the infinite/nonstandard numbers. For a standard formula or function $A(n)$ defined on $N$, the object $^\star A(n)$ is defined on $^\star N$. Let $R$ be the set of real numbers.]

($\Omega$-invariance)

1. For a standard bounded formula $\varphi(n,m)$, and an infinite number $\omega\in \Omega$, the formula $^\star\varphi(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star\varphi(n,\omega)\leftrightarrow {^\star}\varphi(n,\omega')].$$

2. For a standard function $f:N\times N\rightarrow N$, and an infinite number $\omega\in \Omega$, the function $^\star f(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star f(n,\omega)= {^\star}f(n,\omega')].$$

3. For a standard function $F:R\times N\rightarrow R$, and an infinite number $\omega\in \Omega$, the function $^\star F(x,\omega)$ is $\Omega$-invariant if $$(\forall x\in R)(\forall \omega'\in\Omega)[^\star F(x,\omega)\approx {^\star}F(x,\omega')].$$

Note that $\Omega$-invariance is essentially "independence of the choice of infinitesimal".

Now, $\Omega$-CA is the comprehension axiom for $\Omega$-invariant formulas as follows: For all $\Omega$-invariant $^\star\varphi(n,\omega)$, we have $(\exists X^s \subset N)(^\star\varphi(n,\omega) \leftrightarrow n\in X^s)$. Here, the superscript $^s$' refers to the fact that $X^s$ is a standard set.

Recently, Antonio Montalbán and me showed the following:

1. $^\star$RCA$_0+\Omega$-CA is a conservative extension (in the standard language) of RCA$_0$. Here, $^\star$RCA$_0$ is a nonstandard version of $\text{RCA}_0$.

2. In $^\star I\Sigma_1$, $\Omega$-CA implies $\Delta_1^0$-comprehension.

3. $^\star$RCA$_0+\Omega$-CA proves that for every $\Omega$-invariant $^\star F(x,\omega)$, there is a standard $G:R\rightarrow R$ such that $(\forall x\in R)(^\star F(x,\omega)\approx {^\star}G(x)$.

If I am not mistaken, the previous three observations answer your question regarding computable analysis: As long as one produces $\Omega$-invariant functions, the results are computable. (There is/should be some analogue to the Gaifman-Dimitracopoulos theorem here.)

One can refine the above to 'constructive analysis', but explaining that would take up too much space.

One a philosophical note, one might argue that most/all of the infinitesimal calculus used throughout physics is $\Omega$-invariant, and therefore computable.

Three final remarks:

0. There are a number of analogies one can use to compare NSA and constructive/computable analysis. To me, these analogies are quite helpful/insightful. Jasson is right in pointing out his analogy. Not everyone seems to agree on this, however.

1. The above view of NSA is called 'Robinsonian'. The same definitions etc. can be made in Nelson's `internal' framework without any problem.

2. Somehow, mathoverflow does not parse '*' very well: one has to use '\star'.

Nonstandard Analysis (NSA) can be used to prove results in computable/constructive analysis; The central notion is $\Omega$-invariance, defined as follows.

[As usual, the set $N$ consists of the standard/finite/natural numbers; The set ${^{\star}}N$ is an end-extension of $N$ and $\Omega={^{\star}}N\setminus N$ consists of the infinite/nonstandard numbers. For a standard formula or function $A(n)$ defined on $N$, the object $^\star A(n)$ is defined on $^\star N$. Let $R$ be the set of real numbers.]

($\Omega$-invariance)

1. For a standard bounded formula $\varphi(n,m)$, and an infinite number $\omega\in \Omega$, the formula $^\star\varphi(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star\varphi(n,\omega)\leftrightarrow {^\star}\varphi(n,\omega')].$$

2. For a standard function $f:N\times N\rightarrow N$, and an infinite number $\omega\in \Omega$, the function $^\star f(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star f(n,\omega)= {^\star}f(n,\omega')].$$

3. For a standard function $F:R\times N\rightarrow R$, and an infinite number $\omega\in \Omega$, the function $^\star F(x,\omega)$ is $\Omega$-invariant if $$(\forall x\in R)(\forall \omega'\in\Omega)[^\star F(x,\omega)\approx {^\star}F(x,\omega')].$$

Note that $\Omega$-invariance is essentially "independence of the choice of infinitesimal".

Now, $\Omega$-CA is the comprehension axiom for $\Omega$-invariant formulas as follows: For all $\Omega$-invariant $^\star\varphi(n,\omega)$, we have $(\exists X^s \subset N)(^\star\varphi(n,\omega) \leftrightarrow n\in X^s)$. Here, the superscript $^s$' refers to the fact that $X^s$ is a standard set.

Recently, Antonio Montalbán and me showed the following:

1. $^\star$RCA$_0+\Omega$-CA is a conservative extension (in the standard language) of RCA$_0$. Here, $^\star$RCA$_0$ is a nonstandard version of $\text{RCA}_0$.

2. In $^\star I\Sigma_1$, $\Omega$-CA implies $\Delta_1^0$-comprehension.

3. $^\star$RCA$_0+\Omega$-CA proves that for every $\Omega$-invariant $^\star F(x,\omega)$, there is a standard $G:R\rightarrow R$ such that $(\forall x\in R)(^\star F(x,\omega)\approx {^\star}G(x)$.

If I am not mistaken, the previous three observations answer your question regarding computable analysis: As long as one produces $\Omega$-invariant functions, the results are computable. (There is/should be some analogue to the Gaifman-Dimitracopoulos theorem here.)

One can refine the above to 'constructive analysis', but explaining that would take up too much space.

One a philosophical note, one might argue that most/all of the infinitesimal calculus used throughout physics is $\Omega$-invariant, and therefore computable.

Three final remarks:

0. There are a number of analogies one can use to compare NSA and constructive/computable analysis. To me, these analogies are quite helpful/insightful. Jason is right in pointing out his analogy. Not everyone seems to agree on this, however.

1. The above view of NSA is called 'Robinsonian'. The same definitions etc. can be made in Nelson's `internal' framework without any problem.

2. Somehow, mathoverflow does not parse '*' very well: one has to use '\star'.

Nonstandard Analysis (NSA) can be used to prove results in computable/constructive analysis; The central notion is $\Omega$-invariance, defined as follows.

[As usual, the set $N$ consists of the standard/finite/natural numbers; The set ${^{\star}}N$ is an end-extension of $N$ and $\Omega={^{\star}}N\setminus N$ consists of the infinite/nonstandard numbers. For a standard formula or function $A(n)$ defined on $N$, the object $^\star A(n)$ is defined on $^\star N$. Let $R$ be the set of real numbers.]

($\Omega$-invariance)

1. For a standard bounded formula $\varphi(n,m)$, and an infinite number $\omega\in \Omega$, the formula $^\star\varphi(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star\varphi(n,\omega)\leftrightarrow {^\star}\varphi(n,\omega')].$$

2. For a standard function $f:N\times N\rightarrow N$, and an infinite number $\omega\in \Omega$, the function $^\star f(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star f(n,\omega)= {^\star}f(n,\omega')].$$

3. For a standard function $F:R\times N\rightarrow R$, and an infinite number $\omega\in \Omega$, the function $^\star F(x,\omega)$ is $\Omega$-invariant if $$(\forall x\in R)(\forall \omega'\in\Omega)[^\star F(x,\omega)\approx {^\star}F(x,\omega')].$$

Note that $\Omega$-invariance is essentially "independence of the choice of infinitesimal".

Now, $\Omega$-CA is the comprehension axiom for $\Omega$-invariant formulas as follows: For all $\Omega$-invariant $^\star\varphi(n,\omega)$, we have $(\exists X^s \subset N)(^\star\varphi(n,\omega) \leftrightarrow n\in X^s)$. Here, the superscript $^s$' refers to the fact that $X^s$ is a standard set.

Recently, Antonio Montalbán and me showed the following:

1. $^\star$RCA$_0+\Omega$-CA is a conservative extension (in the standard language) of RCA$_0$. Here, $^\star$RCA$_0$ is a nonstandard version of $\text{RCA}_0$.

2. In $^\star I\Sigma_1$, $\Omega$-CA implies $\Delta_1^0$-comprehension.

3. $^\star$RCA$_0+\Omega$-CA proves that for every $\Omega$-invariant $^\star F(x,\omega)$, there is a standard $G:R\rightarrow R$ such that $(\forall x\in R)(^\star F(x,\omega)\approx {^\star}G(x)$.

If I am not mistaken, the previous three observations answer your question regarding computable analysis: As long as one produces $\Omega$-invariant functions, the results are computable. (There is/should be some analogue to the Gaifman-Dimitracopoulos theorem here.)

One can refine the above to 'constructive analysis', but explaining that would take up too much space.

One a philosophical note, one might argue that most/all of the infinitesimal calculus used throughout physics is $\Omega$-invariant, and therefore computable.

Three final remarks:

0. There are a number analogies one can use to compare NSA and constructive/computable analysis. To me, these analogies are quite helpful/insightful. Jasson is right in pointing out his analogy. Not everyone seems to agree on this, however.

1. The above view of NSA is called 'Robinsonian'. The same definitions etc. can be made in Nelson's `internal' framework without any problem.

2. Somehow, mathoverflow does not parse '*' very well: one has to use '\star'.

Nonstandard Analysis (NSA) can be used to prove results in computable/constructive analysis; The central notion is $\Omega$-invariance, defined as follows.

[As usual, the set $N$ consists of the standard/finite/natural numbers; The set ${^{\star}}N$ is an end-extension of $N$ and $\Omega={^{\star}}N\setminus N$ consists of the infinite/nonstandard numbers. For a standard formula or function $A(n)$ defined on $N$, the object $^\star A(n)$ is defined on $^\star N$. Let $R$ be the set of real numbers.]

($\Omega$-invariance)

1. For a standard bounded formula $\varphi(n,m)$, and an infinite number $\omega\in \Omega$, the formula $^\star\varphi(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star\varphi(n,\omega)\leftrightarrow {^\star}\varphi(n,\omega')].$$

2. For a standard function $f:N\times N\rightarrow N$, and an infinite number $\omega\in \Omega$, the function $^\star f(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star f(n,\omega)= {^\star}f(n,\omega')].$$

3. For a standard function $F:R\times N\rightarrow R$, and an infinite number $\omega\in \Omega$, the function $^\star F(x,\omega)$ is $\Omega$-invariant if $$(\forall x\in R)(\forall \omega'\in\Omega)[^\star F(x,\omega)\approx {^\star}F(x,\omega')].$$

Note that $\Omega$-invariance is essentially "independence of the choice of infinitesimal".

Now, $\Omega$-CA is the comprehension axiom for $\Omega$-invariant formulas as follows: For all $\Omega$-invariant $^\star\varphi(n,\omega)$, we have $(\exists X^s \subset N)(^\star\varphi(n,\omega) \leftrightarrow n\in X^s)$. Here, the superscript $^s$' refers to the fact that $X^s$ is a standard set.

Recently, Antonio Montalbán and me showed the following:

1. $^\star$RCA$_0+\Omega$-CA is a conservative extension (in the standard language) of RCA$_0$. Here, $^\star$RCA$_0$ is a nonstandard version of $\text{RCA}_0$.

2. In $^\star I\Sigma_1$, $\Omega$-CA implies $\Delta_1^0$-comprehension.

3. $^\star$RCA$_0+\Omega$-CA proves that for every $\Omega$-invariant $^\star F(x,\omega)$, there is a standard $G:R\rightarrow R$ such that $(\forall x\in R)(^\star F(x,\omega)\approx {^\star}G(x)$.

If I am not mistaken, the previous three observations answer your question regarding computable analysis: As long as one produces $\Omega$-invariant functions, the results are computable. (There is/should be some analogue to the Gaifman-Dimitracopoulos theorem here.)

One can refine the above to 'constructive analysis', but explaining that would take up too much space.

One a philosophical note, one might argue that most/all of the infinitesimal calculus used throughout physics is $\Omega$-invariant, and therefore computable.

Three final remarks:

0. There are a number of analogies one can use to compare NSA and constructive/computable analysis. To me, these analogies are quite helpful/insightful. Jasson is right in pointing out his analogy. Not everyone seems to agree on this, however.

1. The above view of NSA is called 'Robinsonian'. The same definitions etc. can be made in Nelson's `internal' framework without any problem.

2. Somehow, mathoverflow does not parse '*' very well: one has to use '\star'.