i think part of this is a shortcoming of our programming languages. generally, languages allow for the expression of partial graphs, which makes the verification problem technically challenging. my take is that a language that only exposes closed-graph semantics could help bridge the gap between the model and the implementation, even if not absolute.
What you say reminds me of the "Von Neumann Languages Lack Useful Mathematical Properties" section in John Backus's Turing award paper. One of his criticisms of what we would now call imperative languages is that they make it exceedingly difficult to formally prove facts about a program.
rrook · · focus · HN ↗
bunderbunder · · focus · HN ↗
<a href="https://dl.acm.org/doi/epdf/10.1145/359576.359579" rel="nofollow">https://dl.acm.org/doi/epdf/10.1145/359576.359579