[d-us-vb]

You’re confusing the difference between understanding and comprehending. The former is partial but useful within a context, the latter is total and is the result of mastery. One may understand an abstracted interface and how it works from the perspective of what it does in relation to solving a domain problem, but that doesn’t require them to know how it works at the level of any function/procedure’s mechanism.

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.