Hello Jim,
"Don" <nos...@nospam.com> wrote in message
news:i2rk4b$2je...@digitalmars.com...
Jim Balter wrote:
"Walter Bright" <newshou...@digitalmars.com> wrote in message
news:i2nkto$8u...@digitalmars.com...
bearophile wrote:
You have to think about proofs as another (costly) tool to avoid
bugs/bangs,
but not as the ultimate and only tool you have to use (I think
dsimcha
was
trying to say that there are more costly-effective tools. This can
be
true,
but you can't be sure that is right in general).
I want to re-emphasize the point that keeps getting missed.
Building reliable systems is not about trying to make components
that cannot fail. It is about building a system that can TOLERATE
failure of any of its components.
It's how you build safe systems from UNRELIABLE parts. And all
parts are unreliable. All of them. Really. All of them.
You're being religious about this and arguing against a strawman.
While all parts are unreliable, they aren't *equally* unreliable.
Unit tests, contract programming, memory safe access, and other
reliability techniques, *including correctness proofs*, all increase
reliability.
I have to disagree with that. "Correctness proofs" are based on a
total
fallacy. Attempting to proving that a program is correct (on a real
machine, as opposed to a theoretical one) is utterly ridiculous.
I'm genuinely astonished that such an absurd idea ever had any
traction.
I've also heard from people genuinely astonished that such an absurd
idea as that humans evolved from worms ever had any traction.
Well, it is kinda absurd (statistically) unless you assume the existence
of "god" is absurd, at which point the anthropic participial more or less
forces it you into accepting it.
So, I guess that, by dragging in theology, you are asserting by analogy that
the idea of proving a program correct may or may not be absurd, depending
on what axioms you start with?
--
... <IXOYE><
