Given a circuit's blueprints, will it work as advertised? In 1994, Intel had to recall five million of its Pentium processors, due to a bug in the arithmetic circuitry: This cost Intel nearly half a billion dollars, lots of bad publicity, and it happened after intensive testing. Might it have been possible to have a program try to prove the chip's correctness or uncover an error, before casting it in silicon?
Software and hardware companies are increasingly turning to the use of automated proofs, rather than semi-haphazard testing, to verify (parts of) large products correct. However, it is a formidable task, and how to do this is also an active area of research.
There are of course many more examples; one topical popular concern is veriflying certain security properties of electronic voting machines (often provided by vendors who keep their source software a proprietary secret).
Having proofs of correctness is not just comforting; it allows us to save effort (less time testing, and also able to make better optimizations), and prevent recall of faulty products. But: who decides a proof is correct the employee with best SAT scores?l? Is there some trusted way to verify proofs, besides careful inspection by a skilled, yet still error-prone, professional?
Many highly intelligent people are poor thinkers. Many people of average intelligence are skilled thinkers. The power of the car is separate from the way the car is driven. EdwaTd De Bono, consultant, wTiteT, and speakeT (1933-)
- 1195 reads
