pikelet-lang / pikelet

A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧
https://pikelet-lang.github.io/pikelet/
Apache License 2.0
608 stars 26 forks source link

Plans for formalizing the type system and implementation #39

Open brendanzab opened 6 years ago

brendanzab commented 6 years ago

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

Projects

brendanzab commented 6 years ago

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