Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.