4 ms·

>completely removing the need for tests That would be formal verification.

• simiones 6y ago
  Not really. You still need tests to check whether your application is actually achieving its targets in real-world usage, including feature completeness, usability, performance; and how all of these are impacted by the environment (e.g. network issues in a distributed application). Formal verification only tells you that the application matches its spec, given a set of assumptions. Only testing can tell you whether the spec matches the business case, and whether the spec assumptions hold. Paraphrasing Knuth, code that has only been proven correct but not actually tested should always be approached with caution. Edit: Knuth, not Dijkstra
  • seanmcdirmid 6y ago
    Theoretically, formal verification can only tell you as much as can be encoded in a formal spec@.The problem is that no such kind of specs are known to exist (yet, if ever). As a thought experiment, if the informal specs written in English/Chinese or trapped in our head were as incomplete as a formal spec, we wouldn’t even be able to reason about what to test in the first place. @ Then there is the limitation of verification tech of course.
• hinkley 6y ago
  Which from what I’ve seen is way harder and way less accessible than testing. And one of the things I say to anxious coworkers who are struggling with testing is that it’s a lot harder than you think.
• tom_mellior 6y ago
  When I was working with CompCert, I had no problems producing a formally verified compiler that miscompiled its (meager) test suite. Tests are necessary for "formally verified" systems! You might mess up parts of the specs or the model you are verifying against. You can only catch these problems through testing.