Plans for formalizing the type system and implementation

[brendanzab]

Had a nice chat with @pythonesque on Twitter:

I think at this point most people involved in Coq development, at least, agree that a majority of the stuff in it should be in a proof assistant (maybe should have been from the beginning). I strongly recommend you try to prove as much as you possibly can; it'll save you later.

https://twitter.com/awesomeintheory/status/983592526232932352

Apparently lots of the trouble comes in the form of optimizations to the type checking algorithm.

I think it might make sense in the short term to try to keep the implementation as close to the syntax-directed algorithm described in the appendix of the book. For the short term our programs should be small, and speed should be less of a concern for us.

As a precaution, we should also try to ensure certain aspects of our implementation avoid known trouble areas, for example using implicit substitutions, and building up a tangle of mutually recusive definitions/modules/types (although that can be hard to avoid at times in dependent type systems).

In parallel we could:

1. Define the declarative semantics (non-syntax-directed) and prove soundness theorems about that
2. Ensure that the syntax directed semantics match the properties of the declarative semantics
3. Using something fancy like Iris to design an imperative, optimized version of the type checker
4. Ensure that the optimized version matches the properties of the declarative semantics as well

Then we could start carefully porting over the optimizations to the Rust implementation.

Resources

Papers

• Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
• Typed Closure Conversion of the Calculus of Constructions
• Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
• Self-compilation and self-verification
• Verified Compilers for a Multi-Language World
• Fully Abstract Compilation via Universal Embedding
• Linking Types for Multi-Language Software: Have Your Cake and Eat It Too

Projects

• wilbowma/cic-redex
• coq-contribs/coq-in-coq
• Type Preservation and Confluence for a for a predicative Calculus of Construction in Autosubst
• sweirich/corespec
• Milawa ("self-verifying" theorem prover for an ACL2-like logic)
• CertiCoq
• CakeML
• ... - please help us find more!

[brendanzab]

Autosubst looks neat! Here's an example of using it to prove type preservation and confluence for a for a predicative Calculus of Construction.