First: > immediately follows that any non-trivial property of software (such as "does the micro firmware turn the LED on when the camera is on") can also not

First: > immediately follows that any non-trivial property of software (such as "does the micro firmware turn the LED on when the camera is on") can also not be decided. Any non-trivial property of arbitrary software, you mean. It is entirely possible to prove that some software is or isn't "secure", for however you define secure. It's just not possible to do that for arbitrary software. It is entirely possible to (for example) write your micro firmware with an integrated proof that non-trivial properties (like the LED/camera thing you mention) are satisfied. Second: > There is no halting problem in hardware. Actually, there is, kind of. Have you heard of the arbitrator problem? Long story short, analog behavior may propagate arbitrarily far into any digital system. You can make it less common, but you cannot get rid of it. Also: any non-trivial property of arbitrary hardware is also isn't provable. (Otherwise you could solve the halting problem, again)