Dependently typed programming languages seem capable of defining types that express many aspects of a program’s specification. Formal specification in that sen

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.