I like your example, and it's a good one for the specific case. I imagine a more formal proof would involve a reduction of any "non-leaky" abstraction to being

I like your example, and it's a good one for the specific case. I imagine a more formal proof would involve a reduction of any "non-leaky" abstraction to being capable of solving the halting problem, which is already proven impossible.