> You typically can't "raise an error" in such contexts in formal reasoning tools. You could write all your formulas in the Maybe / Option monad (which I guess

> You typically can't "raise an error" in such contexts in formal reasoning tools. You could write all your formulas in the Maybe / Option monad (which I guess is the same as 'introducing a "special" value') but that sounds painful...