I think Dan Bernstein is an absolutist, in the sense that he believes error-free...

cperciva · on April 17, 2013

I'm somewhere between the two of you: I think error-free programs are achievable, but I realize it's a huge amount of work and it's impossible to ever know for certain if you've succeeded. I see capsicum as something to help bridge the gap between "I don't think there are any bugs in here" and "this program is safe to run".

Someone · on April 17, 2013

Classical example of "you never know for certain if you've succeeded": http://en.wikipedia.org/wiki/IEFBR14#History_from_the_RISKS_... (see also the takk page and the refernced http://www.miketaylor.org.uk/tech/oreilly/iefbr14.html for some comments on the veracity of these statements)

merlincorey · on April 17, 2013

There's always the great ivory tower known as Provable Programming.

derleth · on April 18, 2013

Provable Programming provably requires non-Turing-complete languages.

Which isn't an insuperable barrier, to be sure, but it's a big piece of evidence against its practicality in actual commercial environments.

ibotty · on April 18, 2013

why has this been downvoted? if this is wrong, a simple "no, this is wrong. see e.g. blah" would have been nice.

daivd · on April 18, 2013

Diagonal proofs like the Halting Problem say that in general you can not prove properties about all programs in a Turing complete language. Thus, there is a class of troublesome programs.

Likewise there is obviously a great number of programs in Turing complete languages that you can prove properties about. Thus, there is a class of pleasant programs (or [program, property] pairs).

We do not know for certain how many of the programs that we want to write that is in each class. I would venture a guess that >99% of all programs ever written are in the "nice" class. If it is really impossible to reason about some property of a program, why would you think it works?