Le projet a débuté en 2012 lorsque l’une des équipes de JetBrains a développé un éditeur collaboratif en temps réel basé sur la transformation opérationnelle (OT). Avec l’aide de l’assistant de preuve Coq, un algorithme OT approprié a été développé et validé, mais l’intérêt pour la vérification automatisée des preuves et la vérification formelle appliquée à des tâches réelles a conduit à la création d’un groupe de recherche distinct. En 2015, le groupe est passé au développement du langage expérimental HoTT.

Site officiel