From ... Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!bloom-beacon.mit.edu!nycmny1-snh1.gtei.net!nycmny1-snf1.gtei.net!news.gtei.net!colt.net!news.tele.dk!news.tele.dk!small.news.tele.dk!newsfeed1.bredband.com!bredband!uio.no!nntp.uio.no!ifi.uio.no!not-for-mail From: Erik Naggum Newsgroups: comp.lang.lisp Subject: Re: Interest of formal proof Was: Rudeness index was Looking for Lisp compiler Date: 08 Jan 2003 02:02:10 +0000 Organization: Naggum Software, Oslo, Norway Lines: 48 Message-ID: <3250980130956676@erik.naggum.no> References: <4PKO9.164844$6k.3348354@news1.west.cox.net> <3E1299AE.50903@nyc.rr.com> <878yy0bbk0.fsf@localhost.localdomain> <87bs2uc6f1.fsf@thalassa.informatimago.com> <87el7obnl0.fsf_-_@thalassa.informatimago.com> Reply-To: http://naggum.no/erik/contact.html Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: maud.ifi.uio.no 1041991332 28733 129.240.65.208 (8 Jan 2003 02:02:12 GMT) X-Complaints-To: abuse@ifi.uio.no NNTP-Posting-Date: 8 Jan 2003 02:02:12 GMT Mail-Copies-To: never User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 Xref: archiver1.google.com comp.lang.lisp:50043 * Pascal Bourguignon | But until we have a strong AI, this cannot be reproduced automatically | (and anyway, check the current software quality to see what results | are attained this way). While the root cause of crime is obviously the laws, it really sounds like you believe that the system is to blame for individual failures. | If instead we start from formal specifications and formal software | development and verification, this can be implemented in software | with a set of tools that don't amount to strong AI: theorem | proovers, theorem checkers, program generators, some goal directed | search, etc, that could be implemented today. Before you do this, you should to try give some program a program and wait for it to tell you what that program actually does. | (Since he has no formal specifications of his own brains, he would | have quite some difficulties to start such a proof). Do you really believe such hogwash or are you just pretending to be stupid for its effect? | Like in our informal world, where to err is human, perhaps to err | will be software too (while I hope they'll err less). You really have no idea what "to err is human" means, do you? I occasionally entertain a Microsoft "fan" with a discussion on the real problem behind viruses and malicious abuse of their software. I maintain that the problem is not that the software is not perfect or approved or proven correct or any such thing, but that it is not /defensive/ against harmful data. There are basically two ways to build a society of autonomous units: You either design away all the anti-social flaws from the outset and let them go their happy way, or you design every single unit with an /immune system/ that copes with bad guys if and when they exist. The problem is therefore not that some software gets viruses or rotten data, but that it keeps going as if it were completely unaffected by it. Drop the moronic "proof of correctness" and "verification" nonsense and design systems that can actually defend themself from bad input. -- Erik Naggum, Oslo, Norway Act from reason, and failure makes you rethink and study harder. Act from faith, and failure makes you blame someone and push harder.