Sorry, I still don’t understand what you mean by “provide”. Do you mean to say that LC was created without a formal denotational semantics?
I’m not a specialist so perhaps you have something in mind I don’t see, but the semantics of LC precisely provides a sound interpretation relative to beta-(eta)-equivalence, doesn’t it?