5 ms·

There also seems to be some intersection here between type-driven development and Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant https://en.wi

There also seems to be some intersection here between type-driven development and Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant

jshaqaw 4y ago
A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.
chills 4y ago
See also: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- peter_d_sherman 4y ago
  Wowzer! 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 4y ago
    If you're excited about that, you might enjoy https://softwarefoundations.cis.upenn.edu/ 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/ 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.
  - rbonvall 4y ago
    I think you will enjoy this talk: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
    - peter_d_sherman 4y ago
      I did, immensely! Thank you for the excellent link!
  - consilient 4y ago
    > all mathematical proofs are algorithms 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.
    - peter_d_sherman 4y ago
      Let me rephrase then... >all mathematical proofs are algorithms All mathematical proofs consist of a series of steps. >all types are algorithms All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. True if the given input is a member of that Type. False if a given input is not a member of that Type. If the definition of an 'Algorithm' -- is 'a series of steps', then both mathematical proofs and types -- must be Algorithms... If we have any debate -- then we are debating the semantics of "what constitutes a step" -- what rigorously defines it -- and what steps may be permitted when... It may very well be that the Lambda Calculus is the best definition of what constitutes these steps -- but it may very well be that there is a different/better paradigm for looking at them (I don't know myself -- I am trying to determine this)... Here, you might like the following video (graciously submitted by rbonvall!) for an overview of some of the different possible paradigms that these steps -- might be considered in: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

There also seems to be some intersection here between type-driven development and Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant

jshaqaw 4y ago

A huge overlap. Idris is aimed at being a general purpose language with proof assistant characteristics while some of its peers are more theorem provers built with general purpose language characteristics.

chills 4y ago

See also: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

peter_d_sherman 4y ago
Wowzer! 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 4y ago
  If you're excited about that, you might enjoy https://softwarefoundations.cis.upenn.edu/ 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/ 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.
- rbonvall 4y ago
  I think you will enjoy this talk: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
  - peter_d_sherman 4y ago
    I did, immensely! Thank you for the excellent link!
- consilient 4y ago
  > all mathematical proofs are algorithms 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.
  - peter_d_sherman 4y ago
    Let me rephrase then... >all mathematical proofs are algorithms All mathematical proofs consist of a series of steps. >all types are algorithms All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. True if the given input is a member of that Type. False if a given input is not a member of that Type. If the definition of an 'Algorithm' -- is 'a series of steps', then both mathematical proofs and types -- must be Algorithms... If we have any debate -- then we are debating the semantics of "what constitutes a step" -- what rigorously defines it -- and what steps may be permitted when... It may very well be that the Lambda Calculus is the best definition of what constitutes these steps -- but it may very well be that there is a different/better paradigm for looking at them (I don't know myself -- I am trying to determine this)... Here, you might like the following video (graciously submitted by rbonvall!) for an overview of some of the different possible paradigms that these steps -- might be considered in: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU