"retard" <r...@tard.com.invalid> wrote in message
news:i2smf3$2lt...@digitalmars.com...
Thu, 29 Jul 2010 13:22:35 +0000, dsimcha wrote:
== Quote from Don (nos...@nospam.com)'s article
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.
Yea, here's a laundry list of stuff that theory doesn't account for that
can go wrong on real machines:
overflow
rounding error
The proofs help here actually.
compiler bugs
This is a bit unfortunate and unfortunately in some cases there's nothing
you can do - no matter what code you write, the compiler breaks it
fatally.
hardware bugs
In many cases there's nothing you can do. The hardware bug / failure is
fatal. I'm talking about x86 micro-computers here since D isn't that much
suitable yet for other targets. A typical desktop PC has zero redundancy.
A single error in any of the components will kill your program or at
least some part of the user experience.
OS bugs
If your numerics code is fucked up, the proofs really do help. I don't
think your numerics code will use any (problematic non-tested) syscalls.
If the OS breaks independently regardless of your code, there's nothing
you can do. The best way to protect against random OS bugs is to not run
any code on that OS.
I sincerely wish all my numerics code always worked if it was provably
mathematically correct.
I really love digitalmars.D because this is one of the few places
Nah, such appalling ignorance and arrogance is actually quite common.
where
99% of the community has zero experience with other languages, other
paradigms (non-imperative), automatic theorem provers, or anything not
related to D. There's a whole choir against theorem proving now. The
funniest thing is that none of you seem to have any clue about how those
programs work. Has anyone except the almighty Andrei ever even downloaded
a theorem prover?
