Hacker News new | ask | show | jobs
by xmmrm 2257 days ago
>completely removing the need for tests

That would be formal verification.

3 comments

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

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.

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.
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.