But the point I was after everykind of separation we make it will in the end be undone. In that integration the leakyness will make itself apparent.
If you have a reference implementation then your “rule” can’t leak because the code just is what it is. What would be a bug or inconsistency can be redefined to be a feature. But any kind of spesification that is not an instantiation doesn’t contain enough information to construct an instantation yet programs are instances thus instances contain more information than the abstract rules.
I would count that as compiling in to two things.
But the point I was after everykind of separation we make it will in the end be undone. In that integration the leakyness will make itself apparent.
If you have a reference implementation then your “rule” can’t leak because the code just is what it is. What would be a bug or inconsistency can be redefined to be a feature. But any kind of spesification that is not an instantiation doesn’t contain enough information to construct an instantation yet programs are instances thus instances contain more information than the abstract rules.