> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tes

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. You cannot exhaustively test software either - the number of cases to cover are beyond astronomical. The effectiveness of both specification and testing ultimately depend on the same thing: thinking of all the relevant possibilities. If you overlook a possible failure mode, there's no guarantee it will be caught at any phase. The main benefit of formal methods, I think, is that the rigor tends to make such oversights visible. the only people who think formal methods are a magic bullet are those who have not tried them. Likewise, the only people who think more testing (and especially unit testing) is a magic bullet are those who don't understand combinatorial complexity.