4 ms·
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 interestin
by kaashif 4y ago
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 4y agoBut surely there are uncomputable objects which you can make mathematical statements about. How do you encode them into a type signature?
- defrost 4y ago> 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.
- hnews_account_1 4y agoThere 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.