Comment by skybrian
Many interesting statements aren't a property of the code alone. They're a property of the code when it's run in a particular environment. If you want the proof to be portable then it should only make assumptions that are true in any environment.
No assumption holds for all environments.
Posh example: Axiom of choice.