There has been mathematically proven software and the space shuttle came close though that was not proven as such.
Well… If you know what you wish to prove then it’s possible that there exists a logical string that begins with a computer program and ends with it as a necessity. But that’s not really exciting. If you could code in the language of proof-theory, you already have the program. The mathematical proof of a real program is just a translation of the proof into machine code and then showing it goes both ways.
You can potentially prove a space shuttle program will never crash, but you can’t prove the space shuttle won’t crash. Source code is just source code, and bugs aren’t always known to be such without human reflection and real world testing. The translation from intent to code is what was broken in the first place, you actually have to keep applying more intent in order to fix it.
The problem with AGI is that the smartest people in the world write reams trying to say what we even wish to prove, and we’re still sort of unsure. Most utopias are dystopias, and it’s hard to prove a eutopia, because eutopias are scary.
It seems to me that we’re less interested in perfect programs and more interested in programs that are good enough, and there are plenty of those, e.g. some cryptographic software, the mars rover and the Apollo systems, life-critical systems generally, telecom stuff. Of course, there are many notablefailures, too.
If this issue is any indication, there’s risk compensation at play and military seems to use far more brittle designs (of the sort that would not work at all for the commercial software; with 50x the bug rate, if you have that level of fragility the software will crash all the time).
For applications of fewer than 300 LOC, “Fewer than one defect expected” certainly meets a loose definition of “Bug-free”.
As an example of a program with no defects, I put forth the Overpower Scram Logic for a particular pressurized water reactor. It runs on specialized hardware which can be diagrammed fully in the documentation, but is normally shown as a ‘black box’ with several digital and one analog input, and one digital output.
The reality disagrees: the defect rate in bugs/1000 lines of code for high-quality business software is 10-15, for scientific computing is 1-5, and for military applications 0.2-3. See, for example, http://home.comcast.net/~gregorympope/published_papers/Measuring_Good2.doc . This is by no means “bug-free”.
That was the defect rate of software that meets current requirements and budgets.
There has been mathematically proven software and the space shuttle came close though that was not proven as such.
Well… If you know what you wish to prove then it’s possible that there exists a logical string that begins with a computer program and ends with it as a necessity. But that’s not really exciting. If you could code in the language of proof-theory, you already have the program. The mathematical proof of a real program is just a translation of the proof into machine code and then showing it goes both ways.
You can potentially prove a space shuttle program will never crash, but you can’t prove the space shuttle won’t crash. Source code is just source code, and bugs aren’t always known to be such without human reflection and real world testing. The translation from intent to code is what was broken in the first place, you actually have to keep applying more intent in order to fix it.
The problem with AGI is that the smartest people in the world write reams trying to say what we even wish to prove, and we’re still sort of unsure. Most utopias are dystopias, and it’s hard to prove a eutopia, because eutopias are scary.
That link’s 404 for me.
Corrected link (without a period at the end).
fixed.
It seems to me that we’re less interested in perfect programs and more interested in programs that are good enough, and there are plenty of those, e.g. some cryptographic software, the mars rover and the Apollo systems, life-critical systems generally, telecom stuff. Of course, there are many notable failures, too.
If this issue is any indication, there’s risk compensation at play and military seems to use far more brittle designs (of the sort that would not work at all for the commercial software; with 50x the bug rate, if you have that level of fragility the software will crash all the time).
For applications of fewer than 300 LOC, “Fewer than one defect expected” certainly meets a loose definition of “Bug-free”.
As an example of a program with no defects, I put forth the Overpower Scram Logic for a particular pressurized water reactor. It runs on specialized hardware which can be diagrammed fully in the documentation, but is normally shown as a ‘black box’ with several digital and one analog input, and one digital output.