[madmax96]

Dependently typed languages make it even better.

For example, in Lean4:

  def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠ 0) : Nat
    :=
    if denominator > numerator then
      0
    else 
      1 + myDiv (numerator - denominator) denominatorNotZero
  
  -- Example usage.
  example : myDiv 1 (denominator := 1) (by simp) = 1 := rfl
  example : myDiv 120 (denominator := 10) (by simp) = 12 := rfl

You have to submit a proof that the denominator is non-zero in order to use `myDiv`. No monad required ;).