Hacker News Reader

Medicine is fuzzy, software is mostly maths. You can prove your software has no bugs and you increasingly should be proving that. The hard part is knowing if what you prove is what the software is doing.

View on HN

> You can prove your software has no bugs

That very much depends on got you define “bug” and how you specify your product requirements. Also, you have to assume the specs are correct.

The percentage of software that is even in theory provable to be bug free is a miniscule proportion of the software we use on a day to day basis. In many cases, simply the act of writing a proof becomes largely idempotent to building bug free software which is impractical.

That depends on the spec you are proving. If you define bug free as won't overflow any buffers and never follow the NULL pointer it might be possible to prove that much. This would be a useful thing to prove for Postgress - even though it could return garbage for every possible select statement and still pass the above proof. If you want to prove postgres does the right thing as well that is much harder to spec - it might not be worth it.

Reply on news.ycombinator.com