> The project started incidentally in 2012 when one of the teams at JetBrains was developing a collaborative real-time editor based on operational transformation (OT). With the help of Coq proof assistant, a suitable OT algorithm was developed and validated, but the interest in automated proof checking and formal verification as applied to real-world tasks led to a creation of a separate research group. In 2015 the group switched over to the development of the experimental HoTT language.
> The project started incidentally in 2012 when one of the teams at JetBrains was developing a collaborative real-time editor based on operational transformation (OT). With the help of Coq proof assistant, a suitable OT algorithm was developed and validated, but the interest in automated proof checking and formal verification as applied to real-world tasks led to a creation of a separate research group. In 2015 the group switched over to the development of the experimental HoTT language.