>>13
Every program in
Martin-Löf's constructive type theory terminates. Because of
Curry–Howard isomorphism every mathematical formula can be expressed as a type so mathematics are equal power.
Touring completion requires unbounded computation capabilities there fore mathematics not touring complete.
PROVE ME RIGHT