Comment by cjfd
2 years ago
I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier.
For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.