I think it's the possibility of nontermination that leads to unsoundness. You can construct a well-typed program that never produces a result, which means the f

I think it's the possibility of nontermination that leads to unsoundness. You can construct a well-typed program that never produces a result, which means the fact that a program has a particular type does not mean you've proved a particular proposition.