Comment by geraneum

> Couldn’t it very well be that you proved something that wasn't actually your program?

Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.