Can't we just apply a bunch of correctness preserving translations towards a modern PL, perhaps aided by an LLM to keep the source as human readable as possible, while (I'm stressing this) preserving correctness?
You can’t, unless you transform cobol to cobol and run the emulator on aws. It will still manage to fail you in some way
IBM offers just such a service under the WatsonX branding, it's an LLM to convert COBOL to Java: https://www.ibm.com/products/watsonx-code-assistant-z
I work at a company with a large COBOL codebase and this has been mentioned in a few presentations about our modernization efforts.