Yes. And its almost impossible to do this without a huge investment in time and effort, except: If you use languages with FP, and are rigorous, then I believe (possibly wrongly) its actually somewhat simpler to understand because the style of coding in FP exposes much of this "better" than in classic imperative coding

So yes, I think you're right: great dream, hugely hard to do, if not actually impossible in most cases near as damnit, but there are places where program proofs take you to this, Military/Space/Medical needs to know the code calls don't have unexpected outcomes. And language choices which express as "how" you express code, can also help. Probably not enough.