Subject: Re: Interest of formal proof  Was: Rudeness index was Looking for Lisp compiler
From: Erik Naggum <>
Date: 11 Jan 2003 11:26:48 +0000
Newsgroups: comp.lang.lisp
Message-ID: <>

* Thomas Stegen
| That you call "proof of correctness" and verification" moronic
| nonsense is perhaps evidence towards the fact that we do not know
| enough about the software development process to make a judgement
| about the worth of formal proofs.

  But it is not the worth that I am worried about, it is the cost,
  which drives the /net/ worth deep into the red.  This is not
  because of the software /development/ process, but because of the
  /living/ conditions of the developed software -- what it means for
  software to coexist.  

  To create something new in a language that regards all unproven
  statements as if they were hostile, you would have to make each step
  of the expression so minute that the human mind would be incapable
  of accomplishing anything within budget.  We would no longer develop
  software in programming languages, we would spend all our time
  developing programming languages in which it would, someday, be
  possible to prove something useful.

  If we know enough about the problem to prove its specification and
  solution correct, there is no longer any reason to work on it, and
  the solution to the problem should simply be published and taught.
  Actum ne agas.  Move on to the next problem.

  It is not of the software we know too little, it is the real world.
  Human coping strategies are incommensurate with software coping
  strategies.  The belief that mathematical proofs will help software
  live long and prosper is bogus at its root.  Software will be just
  as much blindsided by the unpredictable real world as humans are, it
  will just happen in very different ways.  When humans are overloaded
  with tasks they are unable to complete, they break down, and so do
  computers, but we treat the same problem very differently.  When
  software or even hardware is given bad input, that is just as bad as
  poisoning or infecting humans, but the way humans respond to it is
  by means that have been optimized for survival of the base system
  while the bad input is being dealt with.  Software is allowed to die
  immediately upon encountering certain toxins, and evil software has
  no idea it is infected and go on to contaminate its environment.

  I think proofs of correctness and verification were really good
  ideas in the early days of computing.  Research on the optimal baby
  food for our fledgling computers was the right way to go then.  But
  today, computers have grown up and are extremely powerful, and they
  spend almost all their time waiting for something and have resources
  to spare.  Multics, if it had survived, would be far less complex
  than Unix of today despite the fact that the latter was born out of
  sheer frustration with the "wastefulness" of the former in the eyes
  of the myopic designers.  Today, we can let our computers do much
  more work at runtime than we could mere years ago.  Common Lisp has
  in many ways been eclipsed by the much slower interpreted languages
  that have become popular while it stressed compilation and hardware
  became fast enough to interpret other languages.  Building software
  immune systems would probably be more cost-effective than proving
  code correct.

  The complexity of software and systems that survive bad input is
  many orders of magnitude worse than that of software and systems
  that crash and burn on any bad input.  It necessarily means slower
  execution of (more system overhead for) the overall system, but not
  necessarily slower execution of critical sections.  We already see
  that the time spent satisfying computers that their input is correct
  is a major drag on the software development process.  Why have we
  created computers that are so picky when everything else we have
  created have been adaptive, dynamic systems in comparison?  Is it
  because we somehow think that humans should /not/ intervene when the
  computer makes a mistake or is given bad data, and therefore have
  not developed software that makes this process work well?

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.