> But does it matter? That depends on the application. It probably doesn't most of the time. My point is not that it is always economical to use formal methods

> But does it matter? That depends on the application. It probably doesn't most of the time. My point is not that it is always economical to use formal methods, just that I suspect their cost is overestimated compared to the benefit (because most programmers are simply unfamiliar with FM). > I also don't understand formal methods well, but wouldn't they also be subject to bugs? Yes, they are. There are multiple classes of errors FM are vulnerable to. 1. In FM you prove your code correct with respect to a specification. But you can make errors in the specification too. The arguments for FM are: a) the spec is much smaller than the program, so the opportunity for error is lower, and spec errors are more obvious; b) often if your spec is wrong, you'll find out when you try to prove your algorithm; and c) combining testing with FM is very likely to uncover whatever errors are left. 2. If your proof of correctness is not mechanically verified, then you may still have trivial implementation errors like mixing up variables and the like. 3. If it is mechanically verified, then theoretically there's still opportunity for errors. The verifier might contain a bug, the compiler might contain a bug, the hardware you run the algorithm on might contain a bug, cosmic radiation may flip a bit during the verification/compilation process, invalidating the correctness, etc. I can soapbox about the implications of this but I will only do that when prompted to :) So indeed, there is no method that gives you zero probability of failure. But you can get the probability orders of magnitude lower, which may be worth it depending on what you're working on.