Is nothing enough? [LWN.net]

Is nothing enough?

Posted Apr 28, 2012 22:07 UTC (Sat) by MisterIO (guest, #36192)
In reply to: Is nothing enough? by Company
Parent article: Fuzzing for Security (The Chromium Blog)

That's incorrect. It's de-facto impossible to _prove_ that a piece of software doesn't have bugs, but that doesn't mean that you can't actually write bug-free code. Just talking about theory.

Is nothing enough?

Posted Apr 29, 2012 1:37 UTC (Sun) by mrons (subscriber, #1751) [Link]

I'm reminded of the following quote by Knuth:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

Is nothing enough?

Posted Apr 30, 2012 20:51 UTC (Mon) by quentin.casasnovas (guest, #58238) [Link]

Saying it is
> de-facto impossible to _prove_ that a piece of software doesn't have bugs
does sound a bit strong... Do you have a proof to back-up that somewhat no piece of software can be proven bug-free? I think it is sometimes possible: in synchronous languages for example, using formal analysis.
Think also about pure functions, which could certainly be proven bug-free mathematically. Lambda calculus and functional languages are an extent to that.

Is nothing enough?

Posted May 3, 2012 5:46 UTC (Thu) by Comet (guest, #11646) [Link] (2 responses)

So formal methods do not exist?

Is nothing enough?

Posted May 3, 2012 14:29 UTC (Thu) by nybble41 (subscriber, #55106) [Link] (1 responses)

> So formal methods do not exist?

No, they're just impractical for software of any reasonable complexity. The largest piece of software I've ever heard of which had a formal proof of correctness was a version of the L4 microkernel--essentially not much more than a low-level message-passing interface, with less than 9k lines of C code--and even then the proof is only as good as the requirements defining "correctness".

[1] http://ertos.nicta.com.au/research/l4.verified/

Is nothing enough?

Posted May 4, 2012 5:00 UTC (Fri) by AndreE (guest, #60148) [Link]

Probably of greater interest is this page.

http://ertos.nicta.com.au/research/l4.verified/proof.pml