3 ms·

Well, we can actually _prove_ that mathematics and programs are isomorphic. (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikip

by yaseer 8y ago

Well, we can actually _prove_ that mathematics and programs are isomorphic. (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) You only get glimpses of that correspondence with procedural programming. It's much more apparent with functional programs though.

Ar-Curunir 8y ago
Doing mathematics is really nothing like software programming. Yes, there is an isomorphism between proofs and programs, but that doesn't mean much for the vast world of mathematics outside logic
- marcosdumay 8y ago
  There are isomorphisms between any place of that vast world of mathematics and logic too. Math is also constrained by fitness, not perfection. Just take a look on the number of unproved conjectures we keep around. It's just that the Math community generally places more value on proofs than the programming, but it is a continuous, and there are more tolerant subcomunities of mathematicians and very intolerant ones of programmers too.
  - Ar-Curunir 8y ago
    I didn't mean that mathematicians don't write code; I meant that doing most mathematics isn't anything like doing programming, even when you're programming in Haskell. Just because two things are isomorphic doesn't mean they're used in the same way. For example, programming is formal but rarely rigorous; mathematics is the opposite.
    - marcosdumay 8y ago
      Most mathematicians do work that is very different from most programmers. Some programmers do work that is similar to most mathematicians, and some mathematicians do work that is similar to most programmers. Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.
MrManatee 8y ago
Please correct me if I've misunderstood Curry–Howard, but the way I see it: In mathematics we can take a proposition, and then try to find a proof for it. Depending on the proposition, this can be extremely challenging. And in programming we can write the type of a function, and then try to write some implementation that our type checker will accept. If the function type is complicated enough, then finding _any_ program that has that type can be challenging. And Curry–Howard correspondence shows us that there's a deep connection between trying to find a proof for a proposition and trying to find any program that has a given type. But when I program, then "trying to find any program that has a given type" rarely feels like the main problem I'm trying to solve. Depending on the program, I may want the program to do any of these things: run efficiently, conserve memory, have a good-looking and intuitive user interface, support multiple languages, be secure, be maintainable. If it's a web app, I want it to support multiple browsers. If it's a game, I want the challenge level to be just right. If it's a software instrument, I want it to sound good. You get the idea. So yes, there exists an isomorphism between programs and proofs, but I'm not really sure what to do with it, since the isomorphism doesn't preserve most of the properties I care about.
- mbrock 8y ago
  Dependently typed programming languages seem capable of defining types that express many aspects of a program’s specification. Formal specification in that sense isn’t enough to guarantee that your game is challenging—but it’s an engineering discipline that helps make sure your implementation is correct, and that you have clear and well-defined intentions. Curry-Howard and dependent types is far from the only way to use logic for reasoning about programs! One cool thing I’ve seen is using linear logic to make prototypes of games. Linear logic is good for expressing rules that consume and produce resources, in a way that fits very well with many game rulesets. Thinking of games as logical systems means you can ask questions like “is level 3 possible to finish starting with the items found in level 2?” (A proof could be a sequence of actions that start with those items and eventually reach the level’s end state.) Logical reasoning isn’t the only aspect of software development, just like structural engineering isn’t the only aspect of building houses.
- yaseer 8y ago

by yaseer 8y ago

Ar-Curunir 8y ago

Doing mathematics is really nothing like software programming. Yes, there is an isomorphism between proofs and programs, but that doesn't mean much for the vast world of mathematics outside logic

marcosdumay 8y ago
There are isomorphisms between any place of that vast world of mathematics and logic too. Math is also constrained by fitness, not perfection. Just take a look on the number of unproved conjectures we keep around. It's just that the Math community generally places more value on proofs than the programming, but it is a continuous, and there are more tolerant subcomunities of mathematicians and very intolerant ones of programmers too.
- Ar-Curunir 8y ago
  I didn't mean that mathematicians don't write code; I meant that doing most mathematics isn't anything like doing programming, even when you're programming in Haskell. Just because two things are isomorphic doesn't mean they're used in the same way. For example, programming is formal but rarely rigorous; mathematics is the opposite.
  - marcosdumay 8y ago
    Most mathematicians do work that is very different from most programmers. Some programmers do work that is similar to most mathematicians, and some mathematicians do work that is similar to most programmers. Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.

MrManatee 8y ago

Please correct me if I've misunderstood Curry–Howard, but the way I see it: In mathematics we can take a proposition, and then try to find a proof for it. Depending on the proposition, this can be extremely challenging. And in programming we can write the type of a function, and then try to write some implementation that our type checker will accept. If the function type is complicated enough, then finding _any_ program that has that type can be challenging. And Curry–Howard correspondence shows us that there's a deep connection between trying to find a proof for a proposition and trying to find any program that has a given type. But when I program, then "trying to find any program that has a given type" rarely feels like the main problem I'm trying to solve. Depending on the program, I may want the program to do any of these things: run efficiently, conserve memory, have a good-looking and intuitive user interface, support multiple languages, be secure, be maintainable. If it's a web app, I want it to support multiple browsers. If it's a game, I want the challenge level to be just right. If it's a software instrument, I want it to sound good. You get the idea. So yes, there exists an isomorphism between programs and proofs, but I'm not really sure what to do with it, since the isomorphism doesn't preserve most of the properties I care about.

mbrock 8y ago
Dependently typed programming languages seem capable of defining types that express many aspects of a program’s specification. Formal specification in that sense isn’t enough to guarantee that your game is challenging—but it’s an engineering discipline that helps make sure your implementation is correct, and that you have clear and well-defined intentions. Curry-Howard and dependent types is far from the only way to use logic for reasoning about programs! One cool thing I’ve seen is using linear logic to make prototypes of games. Linear logic is good for expressing rules that consume and produce resources, in a way that fits very well with many game rulesets. Thinking of games as logical systems means you can ask questions like “is level 3 possible to finish starting with the items found in level 2?” (A proof could be a sequence of actions that start with those items and eventually reach the level’s end state.) Logical reasoning isn’t the only aspect of software development, just like structural engineering isn’t the only aspect of building houses.
yaseer 8y ago