Subject: Re: Interest of formal proof Was: Rudeness index was Looking for Lisp compiler From: Erik Naggum <erik@naggum.no> Date: 11 Jan 2003 11:26:48 +0000 Newsgroups: comp.lang.lisp Message-ID: <3251273208239716@naggum.no> * 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.