Do you mean that since the computer is using some of its processing power to analyze its own circuitry, it cannot therefore dedicate 100% of its processing power to any other process running on the system? Or do you mean that it cannot use all of its processing power to analyze its own circuitry, even if there are no other processes running on the system?
The former I agree with, but that is true of any process whatsoever—e.g. if the computer is running a game of solitaire then that process will use up some non-zero amount of processing power, which the computer therefore cannot devote to any other process.
The latter I disagree with. Let’s say that the computer is running an analysis of its circuitry that can be expressed as a SAT problem (as many real-world hardware verification problems can be). So the computer loads the representation of its circuitry, constructs a SAT problem, then begins searching over the possible variable assignments looking for a solution. Why couldn’t the computer dedicate its full capacity at full speed to this search?
for a given set of resources (cpu-time or instruction count, reads/writes/total storage, etc.), there are computations that can be done directly, which cannot be done in an emulator which takes some of those resources.
There is some amount of underlying useful work that’s being done (calculating expected value of hypothetical actions) which is feasible to directly calculate, and infeasible to calculate the calculation.
When the useful work IS the emulation, then of course it’s using it’s full power. But it can’t emulate and verify the emulation/verification (without additional resources).
Why are you talking about emulation? There are lots of ways to analyze a circuit diagram other than emulation. The autonomous car in the story does not use emulation.
That’s an excellent question—I don’t know if the connection between formal proof and emulation/reflection exists anywhere outside of my mind. I believe my arguments hold for the impossibility of proving something without additional resources over just calculating it (possibly using a method that has proofs about it’s correctness, which happened outside the computation itself).
Sure. It can’t use it’s full capacity at full speed.
Do you mean that since the computer is using some of its processing power to analyze its own circuitry, it cannot therefore dedicate 100% of its processing power to any other process running on the system? Or do you mean that it cannot use all of its processing power to analyze its own circuitry, even if there are no other processes running on the system?
The former I agree with, but that is true of any process whatsoever—e.g. if the computer is running a game of solitaire then that process will use up some non-zero amount of processing power, which the computer therefore cannot devote to any other process.
The latter I disagree with. Let’s say that the computer is running an analysis of its circuitry that can be expressed as a SAT problem (as many real-world hardware verification problems can be). So the computer loads the representation of its circuitry, constructs a SAT problem, then begins searching over the possible variable assignments looking for a solution. Why couldn’t the computer dedicate its full capacity at full speed to this search?
for a given set of resources (cpu-time or instruction count, reads/writes/total storage, etc.), there are computations that can be done directly, which cannot be done in an emulator which takes some of those resources.
There is some amount of underlying useful work that’s being done (calculating expected value of hypothetical actions) which is feasible to directly calculate, and infeasible to calculate the calculation.
When the useful work IS the emulation, then of course it’s using it’s full power. But it can’t emulate and verify the emulation/verification (without additional resources).
Why are you talking about emulation? There are lots of ways to analyze a circuit diagram other than emulation. The autonomous car in the story does not use emulation.
That’s an excellent question—I don’t know if the connection between formal proof and emulation/reflection exists anywhere outside of my mind. I believe my arguments hold for the impossibility of proving something without additional resources over just calculating it (possibly using a method that has proofs about it’s correctness, which happened outside the computation itself).