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