[mikedodds]

Author here. This post is definitely more of a problem statement than a solution. I don't think this area gets enough attention and I'd like more people to think about it! However, I think there are some good reasons to think solving this is possible. E.g. Galois have had proofs in CI at AWS for several years that rerun on code changes - you can read about our approach here: https://link.springer.com/chapter/10.1007/978-3-319-96142-2_.... And elsewhere in the comments Talia Ringer posted about her research, which is very promising as well.

I think there's a tight connection between 'proofs the programmer can understand' and self-repair / automation. The aim should really be to clear away a lot of the scaffolding that's currently needed and hand it off to solvers, and leave programmers to do what they are best at, i.e. understand the meaning of the code. Type checking is a great example of a lightweight formal method that disguises most of the sophisticated automation hiding behind the scenes.

[cocoafleck]

I feel obligated to point out that there are tools that effectively repair broken proofs, but they just aren't labeled as such. For example, Frama-C is a program that takes in a simplified written proof (in a C comment language), and then validates it (as in the tedious middle steps) with z3, cvc4, etc. Unfortunately, Frama-C can't handle dynamic memory yet, and it doesn't handle array sizes correctly forcing for loops over memcpys in some cases if you want to prove anything. I wouldn't recommend it for actual usability, but it does seem to "repair" proofs (as in they were never non-broken/whole in the first place).