# Algorithm

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 , follow the instructions in the base case; if , then first find the quotient q' and remainder r' for and , then follow the instructions in the inductive step. Of course, while we are finding and , we may need to also find the quotient and remainder of and , 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!).