Hacker News Reader

This is a bit random, but there are some formal systems for Euclid's elements out there (see, for example https://arxiv.org/abs/0810.4315).

I think it should be possible to implement this in a dependently typed language like Idris, but haven't really worked on this (yet). Any thoughts?

View on HN

Also see this: http://www.michaelbeeson.com/research/CheckEuclid/index.php

It seems a dependently typed language might be overkill, "The proofs described in this paper only need a rather weak logic. There are no function symbols", "only existential quantifiers; universal quantification over the free variables is left implicit."

They wrote a translator then to convert the proofs to HOL, and Coq, you could presumably do the same for e.g. idris

Awesome, this was exactly the type of comment I was hoping for!

Reply on news.ycombinator.com