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.