> Underneath the hood, Logitext interfaces with Coq in order to check the validity of your proof steps. The frontend is written in Haskell and Ur/Web<p>I wonder why not Agda? Or if Coq then why not OCaml? In both cases it would be easier to upstream parts of Logitext in these projects, benefitting everyone.