[tlringer]

These problems are more closely related than you imagine. In particular, when you change a program, there is often necessarily more information you must give the computer in order to make the corresponding change in the proof. That additional burden is creativity, and is in many cases unavoidable.

With good proof repair techniques you can fix the proof almost fully automatically in a way that mimics the change in the program, but then just ask the programmer a few questions to give the needed creativity to fix the proofs. As far as easy to understand goes, then, that "just" comes down to good UX for asking those questions. (Still not solved!)

Here is the state of the art right now (my most recent paper): https://arxiv.org/abs/2010.00774

Lots left to do but the dream is quite realistic.