Subject: Re: self-hosting gc
From: Erik Naggum <erik@naggum.net>
Date: Sat, 09 Mar 2002 00:25:45 GMT
Newsgroups: comp.lang.lisp
Message-ID: <3224622354197752@naggum.net>

* tb+usenet@becket.net (Thomas Bushnell, BSG)
| Why do you want a formal proof for a Lisp system before you accept its
| pointer guarantees, but you don't expect a formal proof for the C
| compiler or your kernel, before you accept their guarantees?

  But has anyone actually asked for a formal proof for a Lisp system?

  Mostly, what I have written and what I understand Tim to be writing is a
  resounding rejection of all the wild claims made by the "proof" and
  "static typing" crowd, namly that such tactics at the source level is
  _sufficient_ to ensure a bug-free and fully operationsl system, and that
  is only necessary because of their attacks on the infrastructure upon
  which we rely today for problems that very few of us believe would go
  away with all that fancy-schmancy type-based proof cruft, which has a lot
  of theoretical values in how to design and not to design software, but
  those crowds are so incredibly snotty about their "superior" theories and
  so absolutely clueless about many real-world issues that simply do not
  fit their theories, and which therefore appear to many to be a case of
  "if the theory does not fit, you must acquit", which so many people who
  have "good theories" resort to in order to purposefully discard those
  parts of reality that are not explainable by their theories.  I mean, I
  know some really smart people who have these incredibly ludicrous ideas
  about how to design and run societies because they flat out refuse to
  believe that bad people exist, and so completely ignore the threat they
  pose and offer no way to deal with anyone who would seize the opportunity
  to do someone harm.  My theory of society-building is that people are
  only polite and friendly and can work together because there are some
  very serious and credible counter-forces that would be applied against
  any real or attempted use of force to begin with, and that translates to
  how computers have to deal with all of those malicious people who do
  _not_ perceive a credible counter-force to their destructive intents and
  to all those _mishaps_ that just happen to software in a very unfriendly
  real world.

///
-- 
  In a fight against something, the fight has value, victory has none.
  In a fight for something, the fight is a loss, victory merely relief.