> Perhaps we can get to a system that produces not just the binary but also a machine-verifiable proof that the binary implements some higher-level language description of the program.

We don't even have a solution to the halting problem, and it probably can't be solved. "Proof it implements a spec" is pure science fiction.

Hard agree that we'd all be better off muting Elon Musk though.