A Mir Formality walkthrough (2022-06-29)

A walkthrough of the Mir formal system, highlighting common issues with predicates and relations, code refactoring, and improvements for better goal categorization, normalization, and user-defined predicate integration.

Key takeaways

Issues with the logic solver’s use of predicates and relations in the Mir formal system.
The need to refactor code to use categorize_goal instead of built-in predicates.
The logic solver should be able to test and categorize goals independently.
User-defined predicates and relations need to be integrated into the categorization process.
Changes to the code to better handle cyclical dependencies and normalization.
The type layer and decal layer need to be reorganized to better integrate with the logic layer.
The code should generate constraints that make equalities hold.
The user-defined relations and predicates need to be handled more explicitly.
The code needs to be refactored to use wrap existing code into the environment.
The type checker needs to be extended to handle co-inductive cycles.
Changes are needed to make the code more robust and error-free.

A Mir Formality walkthrough (2022-06-29)

More talks