> It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases whe

> It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. It's even even easier to write a specification that says "if this case, do this; if that case, do that; otherwise, do whatever". Just use your proof language's implication symbol. (this ==> THIS) && (that ==> THAT), done.