The reason for banning nonterminating functions is different, logical not computational. If you want a programming language to work as a proof checker then you

The reason for banning nonterminating functions is different, logical not computational. If you want a programming language to work as a proof checker then you want its type system to be a consistent logic, so that a program P of type A can be used as a witness that proposition A is true. Using non-terminating computation you can create such witnesses for any type, including whatever you may want to represent "False". So you have an inconsistent (useless) logic.