Comment by ykonstant

Make invalid states unrepresentable, but take care not to make valid states a huge pain in the ass to represent!

I progam in Lean, a language that makes it extremely easy to state requirements and constraints. Using dependent types, you can even reach down into the implementations of function arguments, demand specific ranges for numerics etc. But this imposes a correspondingly large burden on the function caller! If you have a function

    /-! pass : short for pain in the ass -/
    def pass (n : Nat) (h : 0 < n && n < 5) := n^2

the caller must prove that the first argument is in the stated range and provide the proof in the second argument. You can `sorry` out, but then you are not programming with constraints. So you need to balance representability with convenience.

One way to deal with this without utter insanity is to create a certification monad and make these functions monadic, adding certificates to the return type:

    def myfun (args: _) (reqs: _) : (returns : _) (certificates : _) := sorry

and having the monad try to reconcile certificates with requirements, or open a proof block to prove the consistency manually. I want to implement something like this when I get the time, but in any case, be wary of extremes!