Algorithm = Constructive Proof vs Pure Existence Theorem

Recall the following corner stone of 1D Calculus: Bolzano's Theorem (Intermediate Value Theorem): 

• If $f(x)$ is a continuous function on the closed interval $[a,b]$, with $f(a) < 0 < f(b)$, then there exists $\xi \in (a,b)$ such that $f(\xi) = 0$.

This corner stone is presented as a pure existence result and nothing is said about finding a root $\xi$ with $f(\xi )=0$. It is a pure result in the sense that it is not contaminated with possible worries about how to find the root. Pure and solemn. But maybe missing the esssence?

The 1D Calculus book also presents a proof of the theorem as a demonstration of how a mathematical proof can look. The simplest proof is by bisection checking the sign of the midpoint value $f(\frac{a+b}{2})$ to narrow down the question to one half of the interval. Easy to understand and obviously narrowing down to one point $\xi$ where $f(\xi )$ must vanish, according to a step-by-step algorithm easy to express formally as code.

This is an example of a constructive proof as an algorithm. But Bolzano's Theorem in its usual naked form without any dress, throws away all the information coming with the constructive proof.

You may well ask why? Is it because algorithm is work and work is not what a noble mathematician does?

That was the rule  Newton's Cambridge where his Principia publisher Pepys did not know the multiplication, because counting was done by clerks. 

This scheme extends to Calculus with the following corner stones usually stated as pure existence results:

| Intermediate Value Theorem | bisection |

| Fundamental Theorem / existence for $u'=f$ | time-stepping, $dx = v\,dt$ |

| Contraction mapping principle | iterate the map |

| Inverse function theorem, root existence | Newton's method |

| Extreme Value Theorem | descend to the minimum |

The correct form the theorem then appears as the algorithm behind the constructive proof of the theorem helping understanding and also giving a tool. The Body&Soul program brings this idea into real existence. See Leibniz World of Mathematics.

Notice that Calculus essentially consists of a couple of basic algorithms from which a whole of World emerges by computation.