Totality can be split into two separate properties:

- All programs are defined for all inputs (exhaustive)

- All programs terminate/coterminate

The former is becoming more common (like your Rust example), but the latter isn't very widespread. For example, most would consider a function like this to be exhaustive, even though it loops forever when both Ints are non-zero:

  foo : (Int, Int) -> Int
  foo (0, y) = y
  foo (x, y) = foo (y, x)

Proving termination is hard, and often undesirable; e.g. we want servers and operating systems to keep running indefinitely. However, co-termination can be quite easy, e.g. if we define a Delay (co)datatype:

  data Delay t where
    Now   : t -> Delay t
    Later : Delay t -> Delay t

Wrapping recursive calls in 'Later' allows infinite processes, at the cost of some boilerplate (Delay is a monad, if you know what that is):

  foo : (Int, Int) -> Delay Int
  foo (0, y) = Now y
  foo (x, y) = Later (foo (y, x))

Arguments from academic and mathematicians will/may favor provability.

Pure Functional where everything is function composition have more hope of producing a valid mathematical proof for a block of code. CS/Math will favor this over the aspects that get grouped into total programming, which often don't help provability.