This is pretty misleading, isn't it? Idris and Agda, for example, have coinductive types, which you could in principle use to write a "coprogram" that provably never terminates, such as an operating system (where "terminate" really means "put myself into a clean state and then turn off the power"). See e.g. http://blog.sigfpe.com/2007/07/data-and-codata.html and the links therein; Conor McBride is constantly railing about this; see e.g. https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T... .
I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don't magically let you write random non-terminating programs.
Depending on what you want to achieve there are plenty of tricks and techniques to encode a divergent program in a sound dependent-type theory, but the best approach to use will depend on the problem statement.
