Clarification of Python Functional document

Question

I'm rereading this http://docs.python.org/2/howto/functional.html document and hit this line,

'...Unfortunately, proving programs correct is largely impractical and not relevant to Python software. Even trivial programs require proofs that are several pages long; the proof of correctness for a moderately complicated program would be enormous, and few or none of the programs you use daily (the Python interpreter, your XML parser, your web browser) could be proven correct. Even if you wrote down or generated a proof, there would then be the question of verifying the proof; maybe there’s an error in it, and you wrongly believe you’ve proved the program correct.'

/Emphasis mine on the Python interpreter part/

What does that mean that the Python Interpreter cannot be proven correct? Is that because it would be a long proof or that it in principal can't be proven correct, ala Godel like theorem? Is using the Interpreter then a useful fiction that all the while we use it, it could be wrong all the while, and what would being wrong mean? I mean, the interpreter has given me correct answers on integral arithmetic, so far...

Clarification much appreciated.

Answer 1

It can be done (theoretically) but you'd need a full formal specification of the Python language and the Python interpreter internals. After that you'd need to prove the implementation matches the specification and you'd need to prove the specification adheres to all desired properties (e.g., all possible executions behave in certain ways).

As you can see, that's a massive task and not practical. It also involves updating the specification with every commit, patch or configuration change related to the interpreter. So when you've finally proved a version of the Python interpreter correct it would already be out of date.