I'm not convinced this is possible for anything but a small subset of programs. Such a compiler reasoning about a Turing-complete program would certainly be 'AI-hard', as it would have to essentially be a programmer itself.

What I'm interested in is making proof assistants easier to use by improving their inference capabilities, so programmers can verify the correctness of their programs without having to put in orders of magnitude more work...