Last Updated: December 17, 2019
·
122
· Brian Zeligson

All of programming reduces to natural numbers

Hask mod iso <=> Set mod iso <=> Nat

Via Curry-Howard, all computable programs can be expressed as proofs on sets. Sets mod isomorphism are just the natural numbers. All refactorings that preserve cardinality are provably isomorphic transformations.