There's a middle-ground here where the input and output types of a function (informally) denote the pre- and post-conditions and a (correct) program is equivale

There's a middle-ground here where the input and output types of a function (informally) denote the pre- and post-conditions and a (correct) program is equivalent to a proof that your pre-condition implies the post-condition. A function List -> Sorted List can both be considered a proof that lists can be sorted as well as a procedure for sorting lists.