Subject: Re: Interest of formal proof  Was: Rudeness index was Looking for Lisp compiler
From: Erik Naggum <erik@erik.naggum.no>
Date: 08 Jan 2003 02:02:10 +0000
Newsgroups: comp.lang.lisp
Message-ID: <3250980130956676@erik.naggum.no>

* 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.