search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

What is the relationship between redtt and redprl? #471

Closed outlace closed 5 years ago

outlace commented 5 years ago

Is redtt intended to eventually replace redprl?

jonsterling commented 5 years ago

Hi @outlace! In the RedPRL Development Team, our goal is to study implementation techniques for higher-dimensional type theory and determine what works best for our intended applications (both mathematical applications and programming applications). To study this, our first experiment was the RedPRL proof assistant, with which we tested a number of design ideas.

redtt is our second such experiment, based on what we learned from building and using RedPRL, and also representing a close collaboration with our Swedish colleagues, from whom we've also learned a number of ideas about implementation.

I don't think of the current effort so much as "replacing", but as passing to a different stage of the scientific process. There are a lot of ideas from RedPRL that we uphold, and are working on reconstructing in the setting of redtt (including two-level type theory, exact equality, extraction, tactics), but there are other aspects which we changed in redtt that we found to be better adapted to our intended applications (primarily, the question of whether one is constructing proofs using tactics as in redtt, or if one is using tactics to verify the well-typedness of programs as in RedPRL).

I hope this helps! We'll try to add some clarification to the README.