3 ms·

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

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
What you're describing here (and this again is my interpretation) sounds more similar to 'Homotopy Type Theory'. https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory Homotopy Type theory also shows some deep connections between mathematics and programs, as the progress of the theory has bee characterised by building programmatic proofs _first_, to generate new mathematics. That's an inversion of the usual process.

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

What you're describing here (and this again is my interpretation) sounds more similar to 'Homotopy Type Theory'. https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory Homotopy Type theory also shows some deep connections between mathematics and programs, as the progress of the theory has bee characterised by building programmatic proofs _first_, to generate new mathematics. That's an inversion of the usual process.