> You can look at the code,
Of course I can look at the code. Trust me the reason why I introduced the bug wasn't because I was looking at something else at the moment.
> see why you can't prove it correct,
Realistically, this is because the language and the program's design conspire to make proving anything about the program an uphill battle. If the language could perform basic sanity checks (e.g., no attempting to use objects after ownership has been transferred to someone else), then at least I could have a fighting change to manually prove more interesting properties.
> or work backward to see how the code could have gotten to such a state.
Doing this on a per case basis is an incredibly mind-numbing task.
