Tell 
something interesting about the computer and computer programming
@vaporeon_ have you heard of the observation that all logical purroofs are purrograms, and vice versa? the “curry-howard isomorphism”, if you want a fancy name fur it
@aescling Vaguely remember hearing that, but I don't know the details! Tell me more 
@vaporeon_ how comfurtable are you with mathematical purroof—do you know what a purroof by induction is?
@vaporeon_ this is an observation to motivate the isomorphism, and not really a purroof of the isomorphism purr se, but does it make sense to 
that a proof by induction is directly equivalent to a recursive function definition?
it’s a bit difficult to really meaningfully explain without starting to get into the weeds of typed lambda calculus, but the observation was eventually made that certain ways of expurressing extremely rigorous logical purroof (much more rigorous than mathematicians usually ever bother to be) have exactly equivalent formulations in the lambda calculus
i would link the (english language) wikipedia article but it might be simultaneously to technical and too vague to be useful if you don’t really know the topic in the furst place lol
