*BSD News Article 62921


Return to BSD News archive

Path: euryale.cc.adfa.oz.au!newshost.anu.edu.au!harbinger.cc.monash.edu.au!bunyip.cc.uq.oz.au!munnari.OZ.AU!uunet!in2.uu.net!newsfeed.internetmci.com!usenet.eel.ufl.edu!nntp.neu.edu!camelot.ccs.neu.edu!nntp.ccs.neu.edu!albert
From: albert@krakatoa.ccs.neu.edu (Albert Cahalan)
Newsgroups: comp.unix.bsd.freebsd.misc,comp.os.linux.development.system
Subject: Re: The better (more suitable)Unix?? FreeBSD or Linux
Date: 25 Feb 1996 01:29:56 GMT
Organization: Northeastern University, College of Computer Science
Lines: 58
Message-ID: <ALBERT.96Feb24202956@krakatoa.ccs.neu.edu>
References: <4er9hp$5ng@orb.direct.ca> <4f9skh$2og@dyson.iquest.net>
	<4fg8fe$j9i@pell.pell.chi.il.us> <311C5EB4.2F1CF0FB@freebsd.org>
	<4fjodg$o8k@venger.snds.com> <4fo1tu$n31@news.jf.intel.com>
	<DMrCE4.3HF@pe1chl.ampr.org> <4ftjt9$fjs@park.uvsc.edu>
	<DMv8w7.8H4@pe1chl.ampr.org> <4g5ivp$28m@park.uvsc.edu>
	<4gejrb$ogj@floyd.sw.oz.au> <Dn67EK.3nB@pe1chl.ampr.org>
	<4gilab$97u@park.uvsc.edu> <ALBERT.96Feb22220117@krakatoa.ccs.neu.edu>
	<312ECC30.1DDD@wolfenet.com>
NNTP-Posting-Host: krakatoa.ccs.neu.edu
In-reply-to: Mark Hamstra's message of Sat, 24 Feb 1996 00:28:32 -0800
Xref: euryale.cc.adfa.oz.au comp.unix.bsd.freebsd.misc:14958 comp.os.linux.development.system:18766

>>>>> Mark Hamstra <mhamstra@wolfenet.com> writes:

M> Albert Cahalan wrote:

T> Apparently, not having read the documents, you don't realize that it is
T> *impossible* for a conforming implementation to result in the errors you
T> want to attribute to UFS -- short of a unrecoverable hardware failure.  Do
T> you not believe that finite state automatons are deterministic?  I can
T> assure you that they are.
>>
>>  Proofs are great for filesystem development.  They are useless for
>> testing; you should know this.
>> 
>> You can "prove" that something works, but how can you be sure that the code
>> matches your proof?  Yeah, you read it.  So what.  People make bad
>> proofreaders because they see what they expect to see.

M> This is precisely the point of finite state automata and formal languages:
M> you build an abstraction/formalism so simple that it can be mechanically
M> proved correct -- no chance for human error.  You are simply wrong: code
M> can be proven correct.  The fact that typical software engineering practice
M> does not use deterministic proof of code correctness, but relies upon
M> "exhaustive" testing methods doesn't change the science.

Hmm, "you build an abstraction/formalism".  If you do not go directly
from the C (and maybe assembly from .h file) source code, you have
messed up right from the start.  You can not prove code correct if
you test something else instead.  It is easy to make a mistake
when you use human generated junk for your proof.

>> You can prove that a fictional filesystem works, but you can only test,
>> test, and retest a real filesystem.  We're not talking about hello_world.c
>> here.  Even if the code really is good (only God knows for sure), you can
>> hit compiler bugs.

M> Here you raise a valid concern: if your compiler (or for that matter your
M> hardware) has not been proven correct, the determinism of the code is out
M> the window in a formal sense.

>> Maybe you will make a mistake in your reasoning.

M> Again: the operating principle behind deterministic methods is to make
M> abstractions simple and well-defined, so false propositions cannot be
M> proven true.

You _must_ base your proof directly on the source code.
If a human translates, there could be mistakes.

Maybe you could feed the compiler output (assembly code) into
your proof program.  Then your proof might be good - but what will
you use to prove that your proof program works?  Not itself,
not a human...

>> You can _never_ prove that your filesystem is correct, but you can test it.
--

Albert Cahalan
albert@ccs.neu.edu