A proposition is a type. Writing the algorithm which implements the type is the same as proving it.
https://ncatlab.org/nlab/show/propositions+as+types