It's the article that has it backwards. You can deduce true from any premise. In terms of the Curry-Howard isomorphism, I can write a program from any input t

It's the article that has it backwards. You can deduce true from any premise. In terms of the Curry-Howard isomorphism, I can write a program from any input to the one-element type by throwing away the input and returning the one element. I think the previous comment was alluding to "resolution", where you prove a statement true by assuming it is false, and then deriving a contradiction. That only works in classical logic, though.