At the end of the day, the program was asked for by somebody, and that person described what they wanted. Whatever the program does, it can only be as much correct as much unambiguous was the description that conceived it.

The description was most likely given in a natural language, with many assumptions about the shared objective reality.

Today, we have LLMs, which de facto (but with significant flaws) formalize the interpretation of natural language, as well as the shared objective reality we inhabit. They are becoming closer to the truth than any individual human. (Their construction is a wittgensteinian program of sorts.)

So we can take an LLM with the prompt "Respond according to the following specification:" plus the original specification/requirement, in natural language, itself, as a program A.

Then we can take the written program itself, together with the emulator of the machine it runs on, as a program B.

We can feed both of these into some theorem prover - and formally prove that program A and program B give identical outputs on identical inputs. That's most likely the best we can do, ever.

(Or we can, in theory, develop programs this way, as a solution to the following question: Which program, when run on the given platform, gives provably identical answers to program A? That's a general program synthesis problem.)