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.
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.