Return to BSD News archive
#! rnews 3706 bsd Path: euryale.cc.adfa.oz.au!newshost.anu.edu.au!newshost.telstra.net!act.news.telstra.net!psgrain!news.itb.ac.id!news.idola.net.id!uunet!in1.uu.net!nwlink.com!tsunami.ixa.net!news.aa.net!ratty.wolfe.net!news1.wolfe.net!usenet From: Mark Hamstra <mhamstra@wolfenet.com> Newsgroups: comp.unix.bsd.freebsd.misc,comp.os.linux.development.system Subject: Re: The better (more suitable)Unix?? FreeBSD or Linux Date: Sat, 24 Feb 1996 00:28:32 -0800 Organization: Wolfe Internet Access, L.L.C. Lines: 57 Message-ID: <312ECC30.1DDD@wolfenet.com> 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> NNTP-Posting-Host: sea-ts3-p55.wolfenet.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Mailer: Mozilla 2.0GoldB1 (Win95; I) Xref: euryale.cc.adfa.oz.au comp.unix.bsd.freebsd.misc:15010 comp.os.linux.development.system:18817 Albert Cahalan wrote: > > >>>>> "T" == Terry Lambert <terry@lambert.org> writes: > > T> rob@pe1chl.ampr.org (Rob Janssen) wrote: ] Don't bother to tell Terry about > T> your experiences, he will just declare ] your system obsolete and your > T> tools out-of-date. ] Remember: sync metadata updates only work well on > T> *his* system. ] On all others, it is just a drag. > > T> Imagine that... I must have a lot of gall to declare obsolete a file system > T> implementation that doesn't properly conform to the design documents from > T> which it purports to be dervied. > > T> Silly me. > > 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. This is precisely the point of finite state automata and formal languages: you build an abstraction/formalism so simple that it can be mechanically proved correct -- no chance for human error. You are simply wrong: code can be proven correct. The fact that typical software engineering practice does not use deterministic proof of code correctness, but relies upon "exhaustive" testing methods doesn't change the science. > 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. Here you raise a valid concern: if your compiler (or for that matter your hardware) has not been proven correct, the determinism of the code is out the window in a formal sense. > Maybe you will make a mistake in your reasoning. Again: the operating principle behind deterministic methods is to make abstractions simple and well-defined, so false propositions cannot be proven true. > You can _never_ prove that your filesystem is correct, but you can test it. > -- > > Albert Cahalan > albert@ccs.neu.edu