I'm definitely not the first person to do this, but I had an idea a while back for correct by construction FOL terms and formulas in a dependently typed language, and finally got around to playing with it, and it is very cool. The idea is I have a type =Term= representing a term in some first order language, and a type =Formula= representing a formula in that language. Then, through some careful applications of dependent types, it is only possible to construct well-formed formulas. For example, suppose the signature =N= contains a binary function symbol =Plus=, a nullary function symbol (i.e.\nbsp{}constant symbol) =Zero=, and a unary function symbol =S=. Then you can construct the term =Plus(Zero, S(Zero))=, but =Plus(S(Zero(Zero), Zero))= doesn't type check.
Where things start to get really cool is that you can do the same thing with a proof object. So =Proof= is a type representing a proof, but only correct proofs can even be constructed. Typically you'd have representations of terms, formulas, and proofs, but then would have to write code to verify them; verify that the proof is correct and that the terms and formulas are well formed. You can also very easily play with different logics by just tweaking the constructors of =Proof=. For example, by removing the constructor =Contra= from =Proof=, and adding some other constructors that become necessary, you'd have an intuitionist logic. As it stands, the rules and connectives are extremely minimal, with derived rules existing as proofs in the =Logic= module.
I don't really have a goal with this project, and have just been working on it for fun. There's tons more work that can be done. As it stands, this is far less capable/usable than [[https://forgejo.ballcloud.cc/wball/perga][my last proof assistant]], but I think it's pretty cool. It's pretty similar to [[https://github.com/epfl-lara/lisa][lisa]], but with a more trusted kernel and far less usability.
I recently wrote a [[https://blog.ballcloud.cc/idris_fol.html][blog post]] explaining in an overly self-indulgent level of detail how all this works.
* TODOs
** TODO =elimBinder=
=elimBinder= should probably actually take an index to eliminate rather than just always eliminating the outermost index.
** TODO Improve experience working with equality
=EqE= is extremely difficult to use right now, primarily because Idris can't tell that =elimBinder t (inc s) = s=. That and several other lemmas regarding =inc=, =sub=, and =elimBinder= would likely be extremely helpful.
** TODO Consider reworking =Hyp=
If =Hyp : In phi c -> Proof c phi=, then maybe much more data surrounding =c= could be erased, making things more ergonomic, as well as making =Weaken= a theorem, and allowing for easily proving that if =c= and =c'= are permutations of each other, then there exists a =Proof c phi= if and only if =Proof c' phi=, which currently would be an absolute nightmare to prove. This could make using =Hyp= quite a bit more awkward.
** TODO Parser?
This is a /long/ term goal. Making a parser would be quite a challenge, since it also kind of has to come with a proof of correctness in order to work at all with how strict the types are.
** TODO Pretty-Printer
This is much more doable, and would also help quite a bit. It would also be very nice if I could hook it into the repl, so that Idris uses the pretty-printer in holes. Right now, holes are quite difficult to read, since they don't show any abbreviations or anything.
** TODO Unifier
Some sort of unification implementation would make working with equality a lot easier.
