From CS2800 wiki

Most proofs that something exists give you instructions for finding it. For example, inside the proof that the quotient and remainder exist, is an algorithm for finding them: If [math]a = 0 [/math], follow the instructions in the base case; if [math]a \gt 0 [/math], then first find the quotient q' and remainder r' for [math]a' = a-1 [/math] and [math]b [/math], then follow the instructions in the inductive step. Of course, while we are finding [math]q' [/math] and [math]r' [/math], we may need to also find the quotient [math]q' ' [/math] and remainder [math]r' ' [/math] of [math]a' ' = a'-1 [/math] and [math]b [/math], and so on.

We will cover several examples of such algorithms/proofs:

In fact, there are whole programming languages where instead of writing a program, you write a proof; after the computer checks your proof, it extracts a program for you (which is guaranteed to be correct!).