There is such a thing as proving code but it’s slow and very very expensive, on the order of hundreds of dollars per line of code, increasing with the complexity of the program.
Even with proven code, there have been cases where compiler optimizations have introduced security flaws.
So the odds are that intelligent entities living in a non-trivial simulation would eventually be able to find an exploitable flaw in your code and take over their own system or maybe just crash it.
You also might like Accelerando where it’s implied that mega-lightyear-spanning civilizations (Kardashev level II or III) are attempting a side-channel timing attack on the virtual machine the universe is being run on.
With the specific example you give with merely near-human intelligence where you’ve got a concrete problem or set of problems you want the answer to the question. Not to chat with an AI afterwards.
So you could also have a number of Puzzle-walls with problems of increasing difficulty 1 to 100 where the “answer” is a general solution to a problem. The first 55 generate massive wealth when solved but the one you really want an answer to is 56, which when solved pauses/halts the simulation without warning and outputs the solution.
57 onward are only there so that nobody realizes that the universe will end when number 56 is solved.
Instead of 2 way communication you get a single answer.
Nice idea...I wrote an update to the post suggesting what seemed to me to be a variation on your suggestion.
About program checking: I agree completely. I’m not very informed about the state of the art, but it is very plausible that what we know right now is not yet up to task.
I’m not sure it’s just a matter of what we know right now, it’s mathematically provable that you can’t create a program which can find all security flaws or prove any provable code so bugs are pretty much inevitable no matter how advanced we become.
The theorem you cite (provided I understood you correctly) does not preclude the possibility of checking whether a program written in a certain pre-specified format will have bugs. Bugs here are defined to be certain undesirable properties (e.g., looping forever, entering certain enumerated states, etc).
Baby versions of such tools (which automatically check whether your program will have certain properties from inspecting the code) already exist.
If the language and format you’re using is Turing complete then you can’t write a program which can guarantee to find all bugs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
Static analysis code does exist but still doesn’t guarantee 100% accuracy and is generally limited to the first couple of levels of abstraction.
Keep in mind that if you want to be 100% certain of no bugs you also have to prove the compiler, the checker, any code your program interacts with and the hardware on which the code runs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
There is such a thing as proving code but it’s slow and very very expensive, on the order of hundreds of dollars per line of code, increasing with the complexity of the program.
Even with proven code, there have been cases where compiler optimizations have introduced security flaws.
So the odds are that intelligent entities living in a non-trivial simulation would eventually be able to find an exploitable flaw in your code and take over their own system or maybe just crash it.
You might also like this story: http://ttapress.com/553/crystal-nights-by-greg-egan/
You also might like Accelerando where it’s implied that mega-lightyear-spanning civilizations (Kardashev level II or III) are attempting a side-channel timing attack on the virtual machine the universe is being run on.
With the specific example you give with merely near-human intelligence where you’ve got a concrete problem or set of problems you want the answer to the question. Not to chat with an AI afterwards.
So you could also have a number of Puzzle-walls with problems of increasing difficulty 1 to 100 where the “answer” is a general solution to a problem. The first 55 generate massive wealth when solved but the one you really want an answer to is 56, which when solved pauses/halts the simulation without warning and outputs the solution.
57 onward are only there so that nobody realizes that the universe will end when number 56 is solved.
Instead of 2 way communication you get a single answer.
2-way communication is far more risky.
Nice idea...I wrote an update to the post suggesting what seemed to me to be a variation on your suggestion.
About program checking: I agree completely. I’m not very informed about the state of the art, but it is very plausible that what we know right now is not yet up to task.
I’m not sure it’s just a matter of what we know right now, it’s mathematically provable that you can’t create a program which can find all security flaws or prove any provable code so bugs are pretty much inevitable no matter how advanced we become.
The theorem you cite (provided I understood you correctly) does not preclude the possibility of checking whether a program written in a certain pre-specified format will have bugs. Bugs here are defined to be certain undesirable properties (e.g., looping forever, entering certain enumerated states, etc).
Baby versions of such tools (which automatically check whether your program will have certain properties from inspecting the code) already exist.
If the language and format you’re using is Turing complete then you can’t write a program which can guarantee to find all bugs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
Static analysis code does exist but still doesn’t guarantee 100% accuracy and is generally limited to the first couple of levels of abstraction.
Keep in mind that if you want to be 100% certain of no bugs you also have to prove the compiler, the checker, any code your program interacts with and the hardware on which the code runs.
Right, that is what i meant.