Dependently typed languages make it even better. For example, in Lean4: def myDiv (numerator : Nat) {denominator : Nat} (denominatorNotZero : denominator ≠

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 ;).