Logitext – An educational proof assistant for first-order classical logic

logitext.mit.edu

38 pointstheaeolist3 comments

> 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 answer is the 4th link in the article

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.

Reply on news.ycombinator.com