we can basically guarantee that a very short snippet of code (say, a few lines) is secure, right? I’m not sure that’s true, but even if it is, you have to ask:

we can basically guarantee that a very short snippet of code (say, a few lines) is secure, right? I’m not sure that’s true, but even if it is, you have to ask: Which few lines? Let’s say we have the technology that can analyse (say) five lines of code and prove them completely correct and secure. That doesn’t mean you can prove a 500 line program to be secure by running the analysis on each 100 sets of five consecutive lines. Code in one place can affect the logic elsewhere. So now to prove a 500 line program correct, we’d need to analyse every possible combination of 5 lines chosen from the 500 => 255244687600 different proofs to check!