When most people say "a type system can't prove that […]" they mean "I don't know how to make a type system prove that […]".
-
@CarstKoenig
@sforkmann :-) I think it illustrates the point thought. If you drop Turing completeness a type system can prove termination.
@MartenDolk @CarstKoenig @sforkmann with morally correct reasoning (fast & loose) there exists proof of termination within a TC system.
