| ▲ | atq2119 2 hours ago | |
Right. There is something interesting here that could be explored thoughtfully. The hard part is that we rely on compilers being correct, and they mostly are. We have no viable mechanism yet to get the same level of confidence if some LLM-based system writes the binary. 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. Though then the question will be whether we've gained anything, or whether we've just replaced the compiler with something massively more expensive that does the same thing. There's some potential here for the LLM-based system to drive better performance optimizations than a regular compiler could. Of course this isn't what Elon is actually saying, and we'd be better off if fewer people listened to him. | ||
| ▲ | overgard an hour ago | parent [-] | |
> 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. | ||