[kenjackson]

Any program function can be cast as a theorem (although vice-verse is difficult). Proving this theorem is easier than writing the corresponding program function.

And by easier, I mean that the proof is easier to pass off as a correct proof than the program is to pass as a correct program. Of course, writing an actually correct proof is just as difficult as writing an actually correct program -- for the most part. Of course sometimes, due to real world constraints in programs (like dealing with fault tolerance or races for perf) correctness in programs can become magnitudes more difficult.

[jdp23]

I agree in the abstract, but ...

- what's the largest program you've written? - what's the largest program you've proved correctness of?

So in reality, meaningful proofs are much much much harder than writing programs.

[kenjackson]

what's the largest program you've proved correctness of?

But that's the point. With security code, while you may not prove the correctness of it, there's a black hat that's trying to find a counterexample to your "proof".

Whereas for 99% of proofs that are published in the literature no one is trying to prove that there are flaws in the proof. As someone who reviewed CS papers I would always try to really read at least one proof in the paper. Not skim, but really scrutinize it. Probably 75% of the time I could find a problem with the proof. Usually one that was easily corrected, but it was still wrong. But it took substantial effort to do this (which is why I only did one per paper and just read the other proofs).

Some recommended reading: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...