3 ms·
That's a pretty strong statement. Care to provide some examples?
by cantankerous 14y ago
That's a pretty strong statement. Care to provide some examples?
- scott_s 14y agoYou are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.
- cantankerous 14y agoSorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).