🚀 go-pugleaf

mrs@netcom.COM (Morgan Schweers) writes:

[bunch of stuff deleted]
>It's my opinion that a product should work in ALL cases
>before you ship it.  It's also my opinion that this cannot be proven on
>a systems programming level, since the variables are far too complex.
>(As an example, we have one program which can't be used in a certain mode
>with certain other programs, because they use memory in an odd way.  Could
>this have been proven to happen?  Heck no.  Could a 'formal' language prove
>that we can successfully use the disk to swap in portions of our code during
>runtime?  Heck no.  Am I wrong about this?  Someone feel free to tell me of
>a method that will tell me (just from looking at my source) that if I'm running
><program X> in memory, and another program swaps in to do some system checking
>that there will be a memory conflict between the two.  Assume, as is the normal
>case, that I don't have the sourcecode to program X.  Do you even think that
>there is a language in which this *IS* possible?  IMO, hell no.)

Well, we're getting there. J Moore did a proof of correctness for
an assembler, William Bevier did a proof for a small kernel,
and Warren Hunt did one for the gate level implementation
of a chip using the Boyer-Moore prover (see Journal of Automated
Reasoning, December 1989). The prover - an obstinate, nagging proof
checker that won't accept any nonsense - required the proof of
all sorts of lemmata that get close to your problems. For example, it
needed to be proven that the assembler program code could not modify
itself during execution.

I think a lot of people are just scared of formal methods because
they smell like the m-word (*mathematics*), and they are afraid
that they won't understand how to use them and might make fools
out of themselves, so they just try and flame away in the hopes
that formal methods will go away.

"Wat de Buuer nit kunnt, dat frisst he nit" - (loose translation
from the Low German: if the farmer doesn't recognize it, he
won't eat it.)

I quite agree with the opinions expressed in other postings:
Use testing and/or proving as appropriate.

-- 
Debora Weber-Wulff
snail: FU Berlin, ZI Fachdidaktiken, Habelschwerdter Allee 45, W-1000 Berlin 33
email: weberwu@inf.fu-berlin.de, dww@math.fu-berlin.de