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.

▲

dapperdrake 13 hours ago | parent [-]

No assumption holds for all environments.

Posh example: Axiom of choice.

▲

naasking 9 hours ago | parent [-]

There are definitely some assumptions that hold for all environments. For instance, "all resources are finite".

▲

eszed 8 hours ago | parent [-]

Aye, but in many cases a theoretical limit can be ignored in practice. (Stupid example: I need more cooling = "I need more fans", not "I'm running out of air".)

	▲	naasking 2 hours ago \| parent [-]
		Finite resources are a common problem though.