As Natural as 0,1,2
Whether a visitor comes from another place, another planet, or another
plane of being we can be sure that he, she, or it will count just as we
do: though their symbols vary, the numbers are universal. The history
of logic and computing suggests a programming language that is equally
natural. The language, called lambda calculus, is in exact
correspondence with a formulation of the laws of reason, called natural
deduction. Lambda calculus and natural deduction were devised,
independently of each other, around 1930, just before the development
of the first stored program computer. Yet the correspondence between
them was not recognized until decades later, and not published until
1980. Today, languages based on lambda calculus have a few thousand
users. Tomorrow, reliable use of the Internet may depend on languages
with logical foundations.
http://homepages.inf.ed.ac.uk/wadler/topics/history.html#natural
