For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type.\xa0 Under Curry-Howard this means any formula is provable, which is one way to define inconsistency.\xa0 (And logics have to be consistent to be useful.)