Comment by coldcode

Even if this was useful, it presumes the ability to prove a application correct while modifying it. This would only be doable in very limited circumstances not general purpose applications.