3 ms·

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

• xvilka 8y ago
  > 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.
  • sometimesijust 8y ago
    The answer is the 4th link in the article
    • gnulinux 8y ago
      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.