We should be using LLMs to translate from (fuzzy) human specifications to formal specifications (potentially resolving contradictions)

Agreed! This is why having LLMs write assembly or binary, as people suggest, is IMO moving in the wrong direction.

then solving the resulting logic problem with a proper reasoning algorithm. That would also guarantee correctness.

Yes! I.e. write in a high-level programming language, and have a compiler, the reasoning algorithm, output binary code.

It seems like we're already doing this!