The Proof Assistant Coq

I've been learning to use the proof assistant Coq for an Artificial Intelligence project. It is lots of fun to learn about, and it gives a nice concrete way to view the Calculus of Constructions (technically it uses the Predicative Calculus of (Co)Inductive Constructions, apparently).

One of the funny things I've seen about it is that it is possible to get this compilation error: "Universe Inconsistency". Is this not the most intimidating error possible? The universe is inconsistent? Oh god. What do we do? Luckily all this mean is that the stratification of the type Type, which occurs behind the scenes, failed because of some definition. Stratifying Type allows the calculus to remain predicative without making the user manage the infinite hierarchy of universes indexed by the natural numbers.

There are two languages in Coq- Gallina, the term language, and the administration language called the Vernacular.

I need to do a sample project to evaluate the tool, so I've chosen a very simple one- I'm translating the untyped lambda calculus into the system SKI. Its a simple translation on inductive datatypes. I'm not sure how to show that the translation makes any sense- my first thought was some proof of extensional equality, but I don't think thats really possible. I suppose something might be possible, but I can't think of anything that doesn't require reducing lambda terms into a normal form, which is, in general, impossible. I'm sure I'm missing something here.

Coinductive types are pretty neat. They are often infinite, and yet in Coq programs using them must always halt. This is handled by rules on their use that ensure they do not cause some potentially unbounded recursion (co-recursion?). This certainly forbids some programs that would have been terminating, but in this sort of thing we are willing to give up some generality for strong normalization.

Speaking of strong normalization, while the actual logic of the system is intuisionistic, it is possible to do classical proofs. Adding the LEM (Law of the Excluded Middle) to a module does not break the whole system, but I don't know how it interacts with the assurance of termination or the types of proofs possible.

So yea, Coq is pretty awesome. So are the other systems built using the CoC like Adga and Epigram, I only chose Coq because it is a proof assistant and so seems more closely connected to AI to me. It really is amazing to see it prove things, and interactive sessions seem like a conversation with a computer that is capable of fairly complex proof techniques.