Hacker News new | past | comments | ask | show | jobs | submit login

Formal verification and testing are not mutually exclusive and should ideally both be used. If you read this article and conclude that formal verification is the way to go and writing tests is unnecessary, then you are failing to appreciate the concessions Metzger makes. Take e.g.

  but Quark's formal verification doesn't try to show that
  the entire Web browser is correct, and doesn't need to --
  it shows that some insecure behaviors are simply
  impossible. *Those* are much simpler to describe.
Let's assume this is true: we can write interesting programs of relevant size and complexity and prove they are secure. Then we still need a whole bunch of tests to show the program actually does what its users want it to do, because formally specifying that behavior is hard.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: