There’s a huge misunderstanding that pops up in every discussion about “formal methods.” These methods are not perfect silver bullets to guarantee bug-free sof

There’s a huge misunderstanding that pops up in every discussion about “formal methods.” These methods are not perfect silver bullets to guarantee bug-free software forever. They are supposed to be useful engineering tools that help you think and verify your thinking especially for tricky corner cases and interactions. So then it’s a bit like “Why would I think about the code I’m going to write when I could later make a mistake in implementing what I though?” Well, even so it has advantages over not thinking. Not to suggest that “formal methods” are the only way of thinking. They’re just not really what people imagine they are when they criticize them.