With a constructive logic like the one with Coq, you can use functions as proofs of theorems. Briefly, a function is a constructive proof that you can construct

With a constructive logic like the one with Coq, you can use functions as proofs of theorems. Briefly, a function is a constructive proof that you can construct an object of the output type from objects of the input type. This means that you can see types as theorems and functions as proofs of those theorems. But in order to be able to prove useful theorem, you want to enforce that every function does really return an output in all situation.