Comment by kuruczgy

Well, if your language has a sufficiently strong type system (namely, dependent types), you can take proofs of some properties as arguments. Example in Lean:

  def clamp (value min max : Float) {H : min < max} : Float := ...