Hence the term 'deceptively'. Even if a sufficiently advanced proof assistant could internally maintain and propagate constraints up through functions (eg. 'v

Hence the term 'deceptively'. Even if a sufficiently advanced proof assistant could internally maintain and propagate constraints up through functions (eg. 'vec must not alias x'), your point about small imprecisions cascading into large false positives is well made. Bottom up constraints become increasingly difficult to untangle the further away they get from their inception, whereas top down rules such as "no mutable aliasing" are much easier to reason about locally.