In 1936 Alonzo Church tackled a question logicians had circled for decades: is there a method that can decide for any mathematical statement whether it is provable?
To make the question precise he invented a tiny language where everything is a function: the lambda calculus. He used it to prove that no such method exists. Months later a student of his named Alan Turing reached the same conclusion with an imaginary machine. The two proofs were equivalent, and together they drew the line between what a computer can and cannot do.
Church built half the foundation of computer science to settle a question about logic. The lambda calculus he invented is still running today, inside every functional programming language.