> 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
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.
The question still stands because agda handles classical mathematics just fine too. You need to postulate lem, which blocks computation, but that is a non-issue for proof checking.
3 comments
[ 2.9 ms ] story [ 17.1 ms ] threadI 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.