Hacker News new | past | comments | ask | show | jobs | submit login
Logitext – An educational proof assistant for first-order classical logic (mit.edu)
38 points by theaeolist on Aug 2, 2018 | hide | past | web | favorite | 3 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.

Applications are open for YC Winter 2020

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact