It seems to follow that you cannot build a fully general proper-optimisation detector.
So don’t make it fully general. It’s not like that means it’s some near-useless thing that can only run in certain special cases. It’s fine if it works most of the time.
Make it so that if they give the same results, it can usually prove it. If they don’t give the same results, it will never prove it. As such, it will work fine.
Well, ok, just terminate the search for proof after some defined cutoff time, ok. But that may drastically limit the kinds of proof you are able to find.
So don’t make it fully general. It’s not like that means it’s some near-useless thing that can only run in certain special cases. It’s fine if it works most of the time.
Only if you can reliably tell when it didn’t work. :)
Make it so that if they give the same results, it can usually prove it. If they don’t give the same results, it will never prove it. As such, it will work fine.
Well, ok, just terminate the search for proof after some defined cutoff time, ok. But that may drastically limit the kinds of proof you are able to find.
It may. It may not. I don’t know. It may be impossible to optimize a system that much. That’s not my field.