“The Pioneer spaceship includes a plaque designed to communicate with aliens, if any should ever intercept it.

They may find some parts of it easier to interpret than others. A radial diagram shows the distance of 14 pulsars and the center of our galaxy from Sol. Aliens are likely to determine the length of each line is proportional to the distances to each body. Another diagram shows humans in front of a silhouette of Pioneer. If Star Trek gives an accurate conception of alien species, they may respond, “They look just like us, except they lack pubic hair.” However, if the aliens’ perceptual system differs greatly from our own, they may be unable to decipher these squiggles.
What would happen if we tried to communicate with aliens by transmitting a computer program? In the movie Independence Day, the heroes destroy the invading alien mothership by infecting it with a computer virus. Close inspection of the transmitted program shows it contains curly braces; it is written in a dialect of C! It is unlikely that alien species would program in C and unclear that aliens could decipher a program written in C if presented with one.
What about lambda calculus? Propositions as Types tell us lambda calculus is isomorphic to natural deduction. It seems difficult to conceive of alien beings who do not know the fundamentals of logic, and we might expect the problem of deciphering a program written in lambda calculus to be closer to the problem of understanding the radial diagram of pulsars than of understanding the image of a man and a woman on the Pioneer plaque.
We might be tempted to conclude lambda calculus is universal, but first ponder the suitability of the word “universal.” These days, the multiple-worlds interpretation of quantum physics is widely accepted. Scientists imagine that in different universes one might encounter different fundamental constants (such as the strength of gravity or the Planck constant). But easy as it may be to imagine a universe where gravity differs, it is difficult to conceive of a universe where fundamental rules of logic fail to apply. Natural deduction, and hence lambda calculus, should not only be known by aliens throughout our universe but also throughout others. So we may conclude it would be a mistake to characterize lambda calculus as a universal language, because calling it universal would be too limiting.”

*Philip Wadler

Communications of the ACM, Vol. 58 No. 12, Pages 75-84*

http://cacm.acm.org/magazines/2015/12/194626-propositions-as-types