Comment by skybrian
20 hours ago
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.
There are definitely some assumptions that hold for all environments. For instance, "all resources are finite".
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".)
1 reply →