With verification systems like Frama-C and SPARK, which have similar difficulties, I like to think of it as playing "what do I know at this point" until the proof goes through.