> if I had been using Rust, or indeed, formal verification, that wouldn't have helped at all — it would have just written a mathematical proof, proving the correctness of the wrong thing!

This is a well-known issue in formal methods, often referred to as the "formalization gap". It's pretty much an intractable problem, i.e. all we can do is manage it, not solve it.

In fact this issue exists in many fields, often under the name "specification gap" or "specification problem". You'll find versions of that discussed inv economics, architecture (of buildings, not software), etc. In architecture and construction, a high percentage of mistakes that result in lawsuits turn out to be due not to construction, but to specifications that were incorrect in some way.

The bottom line is that there's no perfect formal/mathematical way to go from intent to proof.