3 ms·

I mean, that’s exactly what the Curry-Howard Isomorphism says: that math and programming are equivalent. Both can express and are equivalent to Turing machines

• pron 7y ago
  That is not what the Curry-Howard Isomorphism -- AKA propositions-as-types -- says. Propositions-as-types is the observation that the typing rules of certain type systems follow the inference rules of certain logics (largely because they were designed this way), and that in general typing rules and inference rules can be made to mimic one another, so that a type system can represent propositions in some logic, and type checking represent proof-checking. That arbitrary mathematical proofs can be equivalently made by Turing machines (and conversely, that predicate calculus is Turing complete) is a lemma by Turing, published in the same 1936 paper in which he introduced the notion of computation, Turing machines and proved what today is known as the halting problem.