On: The Mathematical Hacker (2012)

[constantcrying]

>isomorphic

Certainly not every computation is a proof. What statement does:

void f(){ printf("?"); }

prove?

[kaashif → constantcrying]

The fact that you have found a function of type () -> () is a proof that true implies true. This is the Curry-Howard isomorphism.

Not a particularly interesting proof.

[constantcrying → kaashif]

But surely there are uncomputable objects which you can make mathematical statements about. How do you encode them into a type signature?

[hnews_account_1 → constantcrying]

There are no closed form solutions to uncomputable problems. You can encode them in math. You can also encode them in a program. The result is the same.

In fact, the absolute limit of computability is so interesting that people have explored it in the abstract sense. For reference, see busy beaver numbers on Wikipedia or Scott aaronson’s awesome essay on finding the bigger number.

[defrost → constantcrying]

> But surely there are uncomputable objects which you can make mathematical statements about.

Absolutely, one famous example is the halting function that has type (program description, program input) returns boolean.

A symbolic formal system can "reason about reason" and manipulate descriptions of objects that are themselves uncomputable, countably infinte, or even uncountably infinite.

[epgui → constantcrying]

It probably doesn't prove anything more than ∫₀¹ x dx.

Also, just like there are trivial, incorrect or incomplete proofs, there can be trivial, incorrect or incomplete programs.