It seems to me a piece of software is either a formal proof or it's not. So if it's not and we still manage to write robust programs, the natural next question is, to what degree is it okay to knowingly violate the laws? And if you iterate that to the nth, do you end up with Clojure?
> It seems to me a piece of software is either a formal proof or it's not.
That seems like a false dichotomy. Rather I'd say: a program carries a bundle of proven properties with it, but for some programs this will be rich and for others it will be more or less trivial.
> So if it's not and we still manage to write robust programs, the natural next question is, to what degree is it okay to knowingly violate the laws?
To what degree do we actually write robust programs though? Errors are so common we dismiss them and retry or work around without even consciously noticing the error. "Have you tried turning it off and on again" is funny because it's true.
