Is it just me, or is "proof" used in two ways also – the logic and the result? To use the given example, do I need to understand the logic of the Bolzano-Weierstrass proof in order to use it?
A proof furnishes the evidence that a given proposition is attainable (e.g., true).
Truly, you could even see this as being composed of three things
- The proposition
- The "stamp of truth"
- (there's a word from Kant that hits this, but I've forgotten it)
- The proof
Additionally, there may be many proofs of a single proposition, and thus the "stamp of truth" seeks to represent them as a the equivalence class of proofs instead of giving each different method its own identity. This, formally, is the notion of "proof irrelevance". It flies in the face of computation where we care a great deal about algorithmic concerns, but from a correctness perspective perhaps all you need is the "stamp of truth".
One last way to give color here is to note what the advantage of proof _relevance_ is. In particular, if the structure of the proof itself is visible then we can do things such as _transform_ proofs (think: lisp macro). In this way, we can get more flexible systems which are allowed to port much of a proof's mechanism over to a new target automatically.
Of course, mathematicians demand proof relevance because mathematicians (a) don't trust things they can't see and (b) want to cannibalize proofs for their mechanism and to reuse those mechanisms on other problems. Proof irrelevance is often important for computational reasons: we don't want to carry around the burden of proof (literally) if we don't have to.
Note that, according to definition of 'function' most common in math, this is false. A function need not even be implementable.
Aside: As someone trained in math I've always found explanations of type theory "fractally confusing" because of stuff like this: type theorists' words mean something different from my words, and in the explanation of what they do mean, they use words that also mean something different.
> Note that, according to definition of 'function' most common in math, this is false.
The standard definition of function in ZFC is a set of tuples pairing every "input" with an "output", so I think the previous commenter was correct with this reading.
> A function need not even be implementable.
However, if you are alluding to computable functions, then certainly, the story is a lot more interesting!