Proofs are very interesting because they have a computational content. Not only there is a very good language for denoting proofs, but they also carry - especially in a constructive logic - a computational content. There is within a proof we have embedded an algorithm of some sort.
There are even more interesting examples like within a proof that every array of integers can be ordered, there is an algorithm which shows how to order that array. But there is more than just an algorithm embedded in a constructive logic. There is also a proof that that algorithm actually satisfies that specification.
But, remember, it is only in constructive logics that the algorithm that is embedded in the proof has something to do with this specification of the problem, with the statement of that problem. Because if we were to use non-constructive tools, like the proof of excluded middle, well, then, in this case, the kind of algorithm that would be embedded in a proof making use of the proof of excluded middle, would not have necessarily something relevant to the statement of the formula.
I leave as an exercise what is the algorithm that is embedded in Archimede's proof of the existence of infinitely many prime numbers.