That page is decidedly worth reading and re-reading many times in the future...
I think it boils down to the following:
>"Curry–Howard correspondence [...] is the direct relationship between computer programs and mathematical proofs."
And:
>"If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."
In fact, I'm going to go for "full crackpot" here...
If all computer programs are algorithms, and all mathematical proofs are algorithms, and all types are algorithms -- then a "grand unifying theory" between Computer Programs and Mathematics -- looks like this:
It's all Algorithms.
Algorithms on top of algorithms.
You know, like turtles on top of turtles...
This makes sense too, if we think about it...
Algorithms are just series of steps, with given inputs and given outputs.
That is no different than Computer Programs.
And that is no different than Math...
You can call this series of steps an Algorithm, you can call it a Function, you can call it y=f(x), you can call it a Type, you can call it a Computer Program, you can call it a Math Equation, you can call it a logical proposition, and you can use whatever notation and nomenclature you like -- but in the end, in the end, it all boils down to an Algorithm...
A series of steps...
Now, perhaps that series of steps -- uses other series of steps -- perhaps that Algorithm uses other Algorithms, perhaps that function uses other functions, perhaps that Computer Program uses other computer programs, perhaps that Math Equation uses other math equations, etc., etc. --
But in the end, in the end...
It's all a series of rigorously defined steps...
It's all an Algorithm...
Or Algorithm consisting of other Algorithms... (recursively...)
Patterns of steps -- inside of patterns of other steps (again, recursively...)
Anyway, great page, definitely worth reading and re-reading!
Officially you're supposed to download the book and then edit the exercise solutions into it with Emacs (or VSCode, I think), as you can then run the exercises to see if they type-check (i.e., if they're correct!). However, there's also a not-necessarily-up-to-date interactive in-browser version:
I haven't used Idris, so I'd say it's quite possible that working through the Idris book is also just as fun and relevant for understanding the implications of the Curry-Howard correspondence.
They're not. Only constructive proofs have corresponding programs (namely, the program that actually carries out the relevant construction). You can embed nonconstructive proofs indirectly via double-negation translation (computational counterpart: continuation-passing style), but equivalence of classical formulas isn't preserved.
> all types are algorithms
Definitely not the case. Types correspond to propositions, not their proofs.
"Programs as proves" is only a thing in the context of mathematically pure languages.
Almost all programming languages aren't pure.
That's on the other hand's side why prove assistants are very unusable as programming languages; you can't do anything with them usually besides proving stuff. Running actually "useful" code is mostly not possible. Things like Haskell or Idris try to bridge both worlds, but this isn't straight forward. How to actually do anything in a pure programing language is still an open question. Monads are some kludge but not very practicable for most people…
So to summarize: "Normal" programs don't correspond to proves in any way!
peter_d_sherman|3 years ago
That is quite the page...
There is definitely something there!
That page is decidedly worth reading and re-reading many times in the future...
I think it boils down to the following:
>"Curry–Howard correspondence [...] is the direct relationship between computer programs and mathematical proofs."
And:
>"If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."
In fact, I'm going to go for "full crackpot" here...
If all computer programs are algorithms, and all mathematical proofs are algorithms, and all types are algorithms -- then a "grand unifying theory" between Computer Programs and Mathematics -- looks like this:
It's all Algorithms.
Algorithms on top of algorithms.
You know, like turtles on top of turtles...
This makes sense too, if we think about it...
Algorithms are just series of steps, with given inputs and given outputs.
That is no different than Computer Programs.
And that is no different than Math...
You can call this series of steps an Algorithm, you can call it a Function, you can call it y=f(x), you can call it a Type, you can call it a Computer Program, you can call it a Math Equation, you can call it a logical proposition, and you can use whatever notation and nomenclature you like -- but in the end, in the end, it all boils down to an Algorithm...
A series of steps...
Now, perhaps that series of steps -- uses other series of steps -- perhaps that Algorithm uses other Algorithms, perhaps that function uses other functions, perhaps that Computer Program uses other computer programs, perhaps that Math Equation uses other math equations, etc., etc. --
But in the end, in the end...
It's all a series of rigorously defined steps...
It's all an Algorithm...
Or Algorithm consisting of other Algorithms... (recursively...)
Patterns of steps -- inside of patterns of other steps (again, recursively...)
Anyway, great page, definitely worth reading and re-reading!
schoen|3 years ago
https://softwarefoundations.cis.upenn.edu/
Officially you're supposed to download the book and then edit the exercise solutions into it with Emacs (or VSCode, I think), as you can then run the exercises to see if they type-check (i.e., if they're correct!). However, there's also a not-necessarily-up-to-date interactive in-browser version:
https://jscoq.github.io/ext/sf/
I haven't used Idris, so I'd say it's quite possible that working through the Idris book is also just as fun and relevant for understanding the implications of the Curry-Howard correspondence.
consilient|3 years ago
They're not. Only constructive proofs have corresponding programs (namely, the program that actually carries out the relevant construction). You can embed nonconstructive proofs indirectly via double-negation translation (computational counterpart: continuation-passing style), but equivalence of classical formulas isn't preserved.
> all types are algorithms
Definitely not the case. Types correspond to propositions, not their proofs.
rbonvall|3 years ago
still_grokking|3 years ago
"Programs as proves" is only a thing in the context of mathematically pure languages.
Almost all programming languages aren't pure.
That's on the other hand's side why prove assistants are very unusable as programming languages; you can't do anything with them usually besides proving stuff. Running actually "useful" code is mostly not possible. Things like Haskell or Idris try to bridge both worlds, but this isn't straight forward. How to actually do anything in a pure programing language is still an open question. Monads are some kludge but not very practicable for most people…
So to summarize: "Normal" programs don't correspond to proves in any way!