logoalt Hacker News

gpmyesterday at 10:56 PM1 replyview on HN

What I'd like to enable this use of LLMs more recklessly is a compiler with formal methods that lets me guarantee equivalence between the opaque optimized code and something actually understandable.


Replies

MobiusHorizonstoday at 5:33 AM

Equivalence on what metrics? In theory what you are asking for makes sense, but I think it is very hard to actually specify what equivalent means in the context of an optimization process that needs to emit code with observably different behavior. Sometimes (although admittedly rarely) speeding up sections of code can even be undesirable for example branchless code for constant time algorithms that avoid timing or energy side channel leaks, or the much more mundane elimination of signed overflow checks or other undefined behavior quirks.