On: The Mathematical Hacker (2012)

[constantcrying]

Mathematics is not about computation. Certain means of arranging computation are entirely irrelevant to mathematics, computation is a mathematical tool, not an end.

[cs702 → constantcrying]

I never said that mathematics "is about computation."

What I did say is that writing down mathematics is equivalent to writing software.

Both require the use of a formal system.

[constantcrying → cs702]

>I never said that mathematics "is about computation."

But programming is about computation. If mathematics isn't about computation as well, then they are not alike.

>What I did say is that writing down mathematics is equivalent to writing software.

It is not. That is plainly false. E.g. mathematics considers objects which are not computable and makes non-computable calculations with those objects. I am aware that you can encode certain formal mathematics into certain software, but that is like saying cooking is like programming because you can encode recipes as a program.

>Both require the use of a formal system.

So what?

[epgui → constantcrying]

>> What I did say is that writing down mathematics is equivalent to writing software.

> It is not. That is plainly false.

Whether the two look the same or not, maths and computer programs are in fact fundamentally isomorphic. [1]

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[constantcrying → epgui]

>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.