Earlier quoted context omitted.
Personally, I would tell you that whatever understanding you gain may still have bugs. Unless your understanding is as complete as a formal treatment of the code, then there may still be bugs in the code due to shared misunderstandings between author and reviewer. The biggest one is both having an incomplete understanding of what a library function does. So while there may be some overlap, particularly if each person…
If, by your definition of understanding, you can understand something without knowing how it works, then what would be the point in understanding it? Your argument underscores the fact that understanding exists on a spectrum and that deep understanding can be difficult, or even impossible to achieve. Even formal verification seeks to verify certain properties of a system, and doesn't represent anything close to compr…
While it may be true that formal verification doesn’t yield comprehensive understanding of code in certain forms, in a way it does by ensuring the code is only able to perform up to isomorphism with what the domain requires. Further understanding of how it accomplishes that is meaningless due to abstraction. But there are a number of techniques of formal methods that do require comprehensive understanding to be taken as valid, such as the structured proofs Dijkstra was famous for promoting. Also the classic example of Temporal Logic specs don’t compose, so the specifier must design the spec from scratch basically every time. Even using Hoare logic would require one to verify every line and all functions that are called for the purpose of solving a particular problem because of the difficulty of formally describing a function’s behavior in total.
So while I understand where you’re coming from, I do think that for any meaningful understanding regarding code, formal verification will provide it to the verifier. That is, as much as may reasonably be understood from the code is learned during any formal verification process.