I know it seems like one of those Lispers' idiosyncrasies--"discovered" instead of "invented".

I first heard it explained by Philip Wadler, and upon reflection it was one of those "enlightenment" moments that Lispers always go on about: Lambda calculus is a discovery, and should we ever encounter an alien space-faring species, we could read their programs in spite of their alien processing architectures (given that they use a functional language, but let's face it, they have the tech to cross space, they know what they are doing, i.e. they're in the functional camp)

"Propositions as Types" by Philip Wadler, Strange Loop. (https://youtu.be/IOiZatlZtGU?t=1678)