Comment by cayley_graph

It is true that finding the correct specification is a formidable task; knowing what correctness even means is arguably most of the difficulty of programming. However! "Moving bugs up from programs to types" isn't how this shakes out in practice, at all. Another commenter already noted that it's often much easier to communicate your intent through specifications, because you can essentially always say what a computation should do much more simply than you can say exactly how to do it.

I think it's also important not to miss the forest for the trees: even relatively simple specifications like "the compress and decompress functions must be inverses for all inputs" rules out vast classes of bugs in a compression library. This is not a complete specification; for instance, it does not speak about how the decompressor behaves on malicious input. But in my experience, even partial specifications carry the promise of hitting warp speed with LLMs in a way that I haven't seen anywhere else. After a certain level of specification, you have decent guarantees of being able to whole-heartedly forget about the implementation details of the synthesized program. And you get a better-built, more robust program out of it at the end!

The comment at the end of the article about having LLMs directly generate assembly against specifications and letting them rip with finding custom optimizations is the sort of crazy stuff this enables. I really think we're only seeing the tip of the iceberg here. People keep asking what we can do with LLMs that we couldn't before; this is the answer.